![]() |
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 655 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
2 | an4s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: an42s 660 anandis 677 anandirs 678 ax13 2374 nfeqf 2380 frminex 5614 trin2 6078 funprg 6556 funcnvqp 6566 fnun 6615 2elresin 6623 f1cof1 6750 f1coOLD 6752 f1oun 6804 f1oco 6808 fvreseq0 6989 f1mpt 7209 poxp 8061 soxp 8062 poseq 8091 wfr3g 8254 wfrfunOLD 8266 tfrlem7 8330 oeoe 8547 brecop 8750 pmss12g 8808 dif1ennnALT 9222 fiin 9359 tcmin 9678 frr3g 9693 harval2 9934 genpv 10936 genpdm 10939 genpnnp 10942 genpcd 10943 genpnmax 10944 addcmpblnr 11006 ltsrpr 11014 addclsr 11020 mulclsr 11021 addasssr 11025 mulasssr 11027 distrsr 11028 mulgt0sr 11042 addresr 11075 mulresr 11076 axaddf 11082 axmulf 11083 axaddass 11093 axmulass 11094 axdistr 11095 mulgt0 11233 mul4 11324 add4 11376 2addsub 11416 addsubeq4 11417 sub4 11447 muladd 11588 mulsub 11599 mulge0 11674 add20i 11699 mulge0i 11703 mulne0 11798 divmuldiv 11856 rec11i 11897 ltmul12a 12012 mulge0b 12026 zmulcl 12553 uz2mulcl 12852 qaddcl 12891 qmulcl 12893 qreccl 12895 rpaddcl 12938 xmulgt0 13203 xmulge0 13204 ixxin 13282 ge0addcl 13378 ge0xaddcl 13380 fzadd2 13477 serge0 13963 expge1 14006 sqrmo 15137 rexanuz 15231 amgm2 15255 bhmafibid1cn 15349 bhmafibid2cn 15350 mulcn2 15479 dvds2ln 16172 opoe 16246 omoe 16247 opeo 16248 omeo 16249 divalglem6 16281 divalglem8 16283 lcmcllem 16473 lcmgcd 16484 lcmdvds 16485 pc2dvds 16752 catpropd 17590 gimco 19059 efgrelexlemb 19533 psgnghm 20987 pf1ind 21724 tgcl 22322 innei 22479 iunconnlem 22781 txbas 22921 txss12 22959 txbasval 22960 tx1stc 23004 fbunfip 23223 tsmsxp 23509 blsscls2 23863 bddnghm 24093 qtopbaslem 24125 iimulcl 24303 icoopnst 24305 iocopnst 24306 iccpnfcnv 24310 mumullem2 26532 fsumvma 26564 lgslem3 26650 pntrsumbnd2 26918 ajmoi 29803 hvadd4 29981 hvsub4 29982 shsel3 30260 shscli 30262 shscom 30264 chj4 30480 5oalem3 30601 5oalem5 30603 5oalem6 30604 hoadd4 30729 adjmo 30777 adjsym 30778 cnvadj 30837 leopmuli 31078 mdslmd1lem2 31271 chirredlem2 31336 chirredi 31339 cdjreui 31377 addltmulALT 31391 reofld 32139 xrge0iifcnv 32517 funtransport 34619 btwnconn1lem13 34687 btwnconn1lem14 34688 outsideofeu 34719 outsidele 34720 funray 34728 lineintmo 34745 bj-nnfan 35216 bj-nnfor 35218 icoreclin 35831 poimirlem27 36108 heicant 36116 itg2gt0cn 36136 bndss 36248 isdrngo3 36421 riscer 36450 intidl 36491 rimco 40702 unxpwdom3 41425 gbegt5 45960 |
Copyright terms: Public domain | W3C validator |