![]() |
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 2375 nfeqf 2381 frminex 5656 trin2 6122 funprg 6600 funcnvqp 6610 fnun 6661 2elresin 6669 f1cof1 6796 f1coOLD 6798 f1oun 6850 f1oco 6854 fvreseq0 7037 f1mpt 7257 poxp 8111 soxp 8112 poseq 8141 wfr3g 8304 wfrfunOLD 8316 tfrlem7 8380 oeoe 8596 brecop 8801 pmss12g 8860 dif1ennnALT 9274 fiin 9414 tcmin 9733 frr3g 9748 harval2 9989 genpv 10991 genpdm 10994 genpnnp 10997 genpcd 10998 genpnmax 10999 addcmpblnr 11061 ltsrpr 11069 addclsr 11075 mulclsr 11076 addasssr 11080 mulasssr 11082 distrsr 11083 mulgt0sr 11097 addresr 11130 mulresr 11131 axaddf 11137 axmulf 11138 axaddass 11148 axmulass 11149 axdistr 11150 mulgt0 11288 mul4 11379 add4 11431 2addsub 11471 addsubeq4 11472 sub4 11502 muladd 11643 mulsub 11654 mulge0 11729 add20i 11754 mulge0i 11758 mulne0 11853 divmuldiv 11911 rec11i 11952 ltmul12a 12067 mulge0b 12081 zmulcl 12608 uz2mulcl 12907 qaddcl 12946 qmulcl 12948 qreccl 12950 rpaddcl 12993 xmulgt0 13259 xmulge0 13260 ixxin 13338 ge0addcl 13434 ge0xaddcl 13436 fzadd2 13533 serge0 14019 expge1 14062 sqrmo 15195 rexanuz 15289 amgm2 15313 bhmafibid1cn 15407 bhmafibid2cn 15408 mulcn2 15537 dvds2ln 16229 opoe 16303 omoe 16304 opeo 16305 omeo 16306 divalglem6 16338 divalglem8 16340 lcmcllem 16530 lcmgcd 16541 lcmdvds 16542 pc2dvds 16809 catpropd 17650 gimco 19137 efgrelexlemb 19613 psgnghm 21125 pf1ind 21866 tgcl 22464 innei 22621 iunconnlem 22923 txbas 23063 txss12 23101 txbasval 23102 tx1stc 23146 fbunfip 23365 tsmsxp 23651 blsscls2 24005 bddnghm 24235 qtopbaslem 24267 iimulcl 24445 icoopnst 24447 iocopnst 24448 iccpnfcnv 24452 mumullem2 26674 fsumvma 26706 lgslem3 26792 pntrsumbnd2 27060 mulsuniflem 27594 ajmoi 30099 hvadd4 30277 hvsub4 30278 shsel3 30556 shscli 30558 shscom 30560 chj4 30776 5oalem3 30897 5oalem5 30899 5oalem6 30900 hoadd4 31025 adjmo 31073 adjsym 31074 cnvadj 31133 leopmuli 31374 mdslmd1lem2 31567 chirredlem2 31632 chirredi 31635 cdjreui 31673 addltmulALT 31687 reofld 32448 xrge0iifcnv 32902 funtransport 34992 btwnconn1lem13 35060 btwnconn1lem14 35061 outsideofeu 35092 outsidele 35093 funray 35101 lineintmo 35118 bj-nnfan 35615 bj-nnfor 35617 icoreclin 36227 poimirlem27 36504 heicant 36512 itg2gt0cn 36532 bndss 36643 isdrngo3 36816 riscer 36845 intidl 36886 rimco 41091 unxpwdom3 41823 gbegt5 46416 |
Copyright terms: Public domain | W3C validator |