| 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 217 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: an42s 661 anandis 678 anandirs 679 ax13 2380 nfeqf 2386 frminex 5664 trin2 6143 funprg 6620 funcnvqp 6630 fnun 6682 2elresin 6689 f1cof1 6814 f1oun 6867 f1oco 6871 fvreseq0 7058 f1mpt 7281 poxp 8153 soxp 8154 poseq 8183 wfr3g 8347 wfrfunOLD 8359 tfrlem7 8423 oeoe 8637 brecop 8850 pmss12g 8909 dif1ennnALT 9311 fiin 9462 tcmin 9781 frr3g 9796 harval2 10037 genpv 11039 genpdm 11042 genpnnp 11045 genpcd 11046 genpnmax 11047 addcmpblnr 11109 ltsrpr 11117 addclsr 11123 mulclsr 11124 addasssr 11128 mulasssr 11130 distrsr 11131 mulgt0sr 11145 addresr 11178 mulresr 11179 axaddf 11185 axmulf 11186 axaddass 11196 axmulass 11197 axdistr 11198 mulgt0 11338 mul4 11429 add4 11482 2addsub 11522 addsubeq4 11523 sub4 11554 muladd 11695 mulsub 11706 mulge0 11781 add20i 11806 mulge0i 11810 mulne0 11905 divmuldiv 11967 rec11i 12008 ltmul12a 12123 mulge0b 12138 zmulcl 12666 uz2mulcl 12968 qaddcl 13007 qmulcl 13009 qreccl 13011 rpaddcl 13057 xmulgt0 13325 xmulge0 13326 ixxin 13404 ge0addcl 13500 ge0xaddcl 13502 fzadd2 13599 serge0 14097 expge1 14140 sqrmo 15290 rexanuz 15384 amgm2 15408 bhmafibid1cn 15502 bhmafibid2cn 15503 mulcn2 15632 dvds2ln 16326 opoe 16400 omoe 16401 opeo 16402 omeo 16403 divalglem6 16435 divalglem8 16437 lcmcllem 16633 lcmgcd 16644 lcmdvds 16645 pc2dvds 16917 catpropd 17752 gimco 19286 efgrelexlemb 19768 psgnghm 21598 pf1ind 22359 tgcl 22976 innei 23133 iunconnlem 23435 txbas 23575 txss12 23613 txbasval 23614 tx1stc 23658 fbunfip 23877 tsmsxp 24163 blsscls2 24517 bddnghm 24747 qtopbaslem 24779 iimulcl 24966 icoopnst 24969 iocopnst 24970 iccpnfcnv 24975 mumullem2 27223 fsumvma 27257 lgslem3 27343 pntrsumbnd2 27611 mulsuniflem 28175 readdscl 28431 remulscllem2 28433 remulscl 28434 ajmoi 30877 hvadd4 31055 hvsub4 31056 shsel3 31334 shscli 31336 shscom 31338 chj4 31554 5oalem3 31675 5oalem5 31677 5oalem6 31678 hoadd4 31803 adjmo 31851 adjsym 31852 cnvadj 31911 leopmuli 32152 mdslmd1lem2 32345 chirredlem2 32410 chirredi 32413 cdjreui 32451 addltmulALT 32465 reofld 33372 xrge0iifcnv 33932 funtransport 36032 btwnconn1lem13 36100 btwnconn1lem14 36101 outsideofeu 36132 outsidele 36133 funray 36141 lineintmo 36158 bj-nnfan 36749 bj-nnfor 36751 icoreclin 37358 poimirlem27 37654 heicant 37662 itg2gt0cn 37682 bndss 37793 isdrngo3 37966 riscer 37995 intidl 38036 rimco 42528 unxpwdom3 43107 gbegt5 47748 |
| Copyright terms: Public domain | W3C validator |