![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > an4s | Structured version Visualization version GIF version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an4s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
an4s | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an4 900 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
2 | an4s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
3 | 1, 2 | sylbi 207 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: an42s 905 anandis 908 anandirs 909 ax13 2394 nfeqf 2446 frminex 5246 trin2 5677 funprg 6101 funcnvqp 6113 fnun 6158 2elresin 6163 f1co 6272 f1oun 6318 f1oco 6321 fvreseq0 6481 f1mpt 6682 poxp 7458 soxp 7459 wfr3g 7583 wfrfun 7595 tfrlem7 7649 oeoe 7850 brecop 8009 pmss12g 8052 dif1en 8360 fiin 8495 tcmin 8792 harval2 9033 genpv 10033 genpdm 10036 genpnnp 10039 genpcd 10040 genpnmax 10041 addcmpblnr 10102 ltsrpr 10110 addclsr 10116 mulclsr 10117 addasssr 10121 mulasssr 10123 distrsr 10124 mulgt0sr 10138 addresr 10171 mulresr 10172 axaddf 10178 axmulf 10179 axaddass 10189 axmulass 10190 axdistr 10191 mulgt0 10327 mul4 10417 add4 10468 2addsub 10507 addsubeq4 10508 sub4 10538 muladd 10674 mulsub 10685 mulge0 10758 add20i 10783 mulge0i 10787 mulne0 10881 divmuldiv 10937 rec11i 10978 ltmul12a 11091 mulge0b 11105 zmulcl 11638 uz2mulcl 11979 qaddcl 12017 qmulcl 12019 qreccl 12021 rpaddcl 12067 xmulgt0 12326 xmulge0 12327 ixxin 12405 ge0addcl 12497 ge0xaddcl 12499 fzadd2 12589 serge0 13069 expge1 13111 sqrmo 14211 rexanuz 14304 amgm2 14328 mulcn2 14545 dvds2ln 15236 opoe 15309 omoe 15310 opeo 15311 omeo 15312 divalglem6 15343 divalglem8 15345 lcmcllem 15531 lcmgcd 15542 lcmdvds 15543 pc2dvds 15805 catpropd 16590 gimco 17931 efgrelexlemb 18383 pf1ind 19941 psgnghm 20148 tgcl 20995 innei 21151 iunconnlem 21452 txbas 21592 txss12 21630 txbasval 21631 tx1stc 21675 fbunfip 21894 tsmsxp 22179 blsscls2 22530 bddnghm 22751 qtopbaslem 22783 iimulcl 22957 icoopnst 22959 iocopnst 22960 iccpnfcnv 22964 mumullem2 25126 fsumvma 25158 lgslem3 25244 pntrsumbnd2 25476 wlknwwlksnfun 27018 ajmoi 28044 hvadd4 28223 hvsub4 28224 shsel3 28504 shscli 28506 shscom 28508 chj4 28724 5oalem3 28845 5oalem5 28847 5oalem6 28848 hoadd4 28973 adjmo 29021 adjsym 29022 cnvadj 29081 leopmuli 29322 mdslmd1lem2 29515 chirredlem2 29580 chirredi 29583 cdjreui 29621 addltmulALT 29635 reofld 30170 xrge0iifcnv 30309 poseq 32080 frr3g 32106 frrlem5c 32113 funtransport 32465 btwnconn1lem13 32533 btwnconn1lem14 32534 outsideofeu 32565 outsidele 32566 funray 32574 lineintmo 32591 icoreclin 33534 poimirlem27 33767 heicant 33775 itg2gt0cn 33796 bndss 33916 isdrngo3 34089 riscer 34118 intidl 34159 unxpwdom3 38185 gbegt5 42177 |
Copyright terms: Public domain | W3C validator |