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 656 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃))) | |
2 | an4s.1 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
3 | 1, 2 | sylbi 220 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: an42s 661 anandis 678 anandirs 679 ax13 2374 nfeqf 2380 frminex 5528 trin2 5985 funprg 6431 funcnvqp 6441 fnun 6487 2elresin 6495 f1cof1 6623 f1coOLD 6625 f1oun 6677 f1oco 6680 fvreseq0 6855 f1mpt 7070 poxp 7892 soxp 7893 wfr3g 8050 wfrfun 8062 tfrlem7 8116 oeoe 8324 brecop 8489 pmss12g 8547 dif1enALT 8904 fiin 9035 tcmin 9354 frr3g 9369 harval2 9610 genpv 10610 genpdm 10613 genpnnp 10616 genpcd 10617 genpnmax 10618 addcmpblnr 10680 ltsrpr 10688 addclsr 10694 mulclsr 10695 addasssr 10699 mulasssr 10701 distrsr 10702 mulgt0sr 10716 addresr 10749 mulresr 10750 axaddf 10756 axmulf 10757 axaddass 10767 axmulass 10768 axdistr 10769 mulgt0 10907 mul4 10997 add4 11049 2addsub 11089 addsubeq4 11090 sub4 11120 muladd 11261 mulsub 11272 mulge0 11347 add20i 11372 mulge0i 11376 mulne0 11471 divmuldiv 11529 rec11i 11570 ltmul12a 11685 mulge0b 11699 zmulcl 12223 uz2mulcl 12519 qaddcl 12558 qmulcl 12560 qreccl 12562 rpaddcl 12605 xmulgt0 12870 xmulge0 12871 ixxin 12949 ge0addcl 13045 ge0xaddcl 13047 fzadd2 13144 serge0 13627 expge1 13669 sqrmo 14812 rexanuz 14906 amgm2 14930 bhmafibid1cn 15024 bhmafibid2cn 15025 mulcn2 15154 dvds2ln 15847 opoe 15921 omoe 15922 opeo 15923 omeo 15924 divalglem6 15956 divalglem8 15958 lcmcllem 16150 lcmgcd 16161 lcmdvds 16162 pc2dvds 16429 catpropd 17209 gimco 18669 efgrelexlemb 19137 psgnghm 20539 pf1ind 21268 tgcl 21863 innei 22019 iunconnlem 22321 txbas 22461 txss12 22499 txbasval 22500 tx1stc 22544 fbunfip 22763 tsmsxp 23049 blsscls2 23399 bddnghm 23621 qtopbaslem 23653 iimulcl 23831 icoopnst 23833 iocopnst 23834 iccpnfcnv 23838 mumullem2 26059 fsumvma 26091 lgslem3 26177 pntrsumbnd2 26445 ajmoi 28936 hvadd4 29114 hvsub4 29115 shsel3 29393 shscli 29395 shscom 29397 chj4 29613 5oalem3 29734 5oalem5 29736 5oalem6 29737 hoadd4 29862 adjmo 29910 adjsym 29911 cnvadj 29970 leopmuli 30211 mdslmd1lem2 30404 chirredlem2 30469 chirredi 30472 cdjreui 30510 addltmulALT 30524 reofld 31255 xrge0iifcnv 31594 poseq 33536 funtransport 34067 btwnconn1lem13 34135 btwnconn1lem14 34136 outsideofeu 34167 outsidele 34168 funray 34176 lineintmo 34193 bj-nnfan 34664 bj-nnfor 34666 icoreclin 35262 poimirlem27 35539 heicant 35547 itg2gt0cn 35567 bndss 35679 isdrngo3 35852 riscer 35881 intidl 35922 unxpwdom3 40621 gbegt5 44884 |
Copyright terms: Public domain | W3C validator |