Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5ibrcom | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
Ref | Expression |
---|---|
syl5ibr.1 | ⊢ (𝜑 → 𝜃) |
syl5ibr.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5ibrcom | ⊢ (𝜑 → (𝜒 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ibr.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
2 | syl5ibr.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | syl5ibr 145 | . 2 ⊢ (𝜒 → (𝜑 → 𝜓)) |
4 | 3 | com12 27 | 1 ⊢ (𝜑 → (𝜒 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimprcd 149 elsn2g 3404 preqr1g 3537 opth1 3973 euotd 3991 tz7.2 4091 reusv3 4192 alxfr 4193 reuhypd 4203 ordsucim 4226 suc11g 4281 nlimsucg 4290 onpsssuc 4295 xpsspw 4450 funcnvuni 4968 fvmptdv2 5260 foco2 5318 fsn 5335 fconst2g 5376 funfvima 5390 isores3 5455 eusvobj2 5498 ovmpt2dv2 5634 ovelrn 5649 f1opw2 5706 suppssfv 5708 suppssov1 5709 nnmordi 6089 nnmord 6090 qsss 6165 eroveu 6197 th3qlem1 6208 en1bg 6280 addnidpig 6434 enq0tr 6532 prcdnql 6582 prcunqu 6583 genipv 6607 genpelvl 6610 genpelvu 6611 distrlem5prl 6684 distrlem5pru 6685 aptiprlemu 6738 mulid1 7024 ltne 7103 cnegex 7189 creur 7911 creui 7912 cju 7913 nnsub 7952 un0addcl 8215 un0mulcl 8216 zaddcl 8285 elz2 8312 qmulz 8558 qre 8560 qnegcl 8571 xrltne 8729 iccid 8794 fzsn 8929 fzsuc2 8941 fz1sbc 8958 elfzp12 8961 iseqid3 9245 shftlem 9417 replim 9459 sqrtsq 9642 absle 9685 bj-peano4 10080 |
Copyright terms: Public domain | W3C validator |