![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2an2r | GIF version |
Description: syl2anr 290 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Ref | Expression |
---|---|
syl2an2r.1 | ⊢ (𝜑 → 𝜓) |
syl2an2r.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
syl2an2r.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl2an2r | ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an2r.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2an2r.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
3 | syl2an2r.3 | . . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
4 | 1, 2, 3 | syl2an 289 | . 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜒)) → 𝜏) |
5 | 4 | anabss5 578 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: op1stbg 4494 mapen 6864 fival 6987 supelti 7019 supmaxti 7021 infminti 7044 xnegdi 9886 frecuzrdgsuc 10432 hashunlem 10802 2zsupmax 11252 xrmin1inf 11293 serf0 11378 fsumabs 11491 binomlem 11509 cvgratz 11558 efcllemp 11684 ef0lem 11686 tannegap 11754 modm1div 11825 divalglemnqt 11943 lcmid 12098 hashdvds 12239 prmdivdiv 12255 odzcllem 12260 reumodprminv 12271 nnnn0modprm0 12273 pythagtrip 12301 pcmpt 12359 pockthg 12373 4sqlem9 12402 ennnfonelemkh 12431 ctinf 12449 nninfdclemcl 12467 nninfdclemp1 12469 setsslid 12531 imasival 12749 imasaddflemg 12759 grpinvalem 12827 issubmnd 12869 isgrpinv 12964 grpinvssd 12987 imasgrp 13019 mulgnndir 13057 subginv 13086 subginvcl 13088 ghmpreima 13166 conjnsg 13181 srgidmlem 13293 ringidmlem 13337 imasring 13375 dvdsr01 13415 unitnegcl 13441 01eq0ring 13497 issubrng2 13518 subrginv 13545 subrgunit 13547 aprsym 13561 lmodvneg1 13607 lspsn 13693 isridlrng 13759 lidl0cl 13760 rspcl 13768 rspssid 13769 rnglidlmmgm 13773 2idlcpblrng 13799 quscrng 13808 topbas 13964 tgrest 14066 txss12 14163 cnplimclemle 14534 efltlemlt 14592 coseq0q4123 14652 lgsval 14802 lgscllem 14805 neapmkvlem 15213 |
Copyright terms: Public domain | W3C validator |