![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylbir | GIF version |
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sylbir.1 | ⊢ (𝜓 ↔ 𝜑) |
sylbir.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
sylbir | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbir.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | biimpri 132 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylbir.2 | . 2 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 14 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3imtr3i 199 3ori 1246 19.30dc 1574 nf4r 1617 cbvexh 1696 equveli 1700 sbequilem 1777 sb5rf 1791 nfsbxy 1878 nfsbxyt 1879 sbcomxyyz 1906 dvelimALT 1946 dvelimfv 1947 dvelimor 1954 mo2n 1988 mo23 2001 2exeu 2052 bm1.1 2085 necon1idc 2320 sbhypf 2690 vtocl2 2696 vtocl3 2697 reu6 2826 rmo2ilem 2950 uneqin 3274 abn0r 3334 inelcm 3370 vdif0im 3375 difrab0eqim 3376 r19.3rm 3398 r19.9rmv 3401 difprsn1 3606 intminss 3743 disjnim 3866 bm1.3ii 3989 intexabim 4017 copsex2g 4106 opelopabt 4122 eusv2nf 4315 reusv3i 4318 onintrab2im 4372 ordtri2orexmid 4376 setindel 4391 onsucuni2 4417 ordtri2or2exmid 4424 zfregfr 4426 tfi 4434 mosubopt 4542 eqrelrel 4578 xpiindim 4614 opeliunxp2 4617 opelrn 4711 issref 4857 xpmlem 4895 rnxpid 4909 ssxpbm 4910 relcoi2 5005 unixpm 5010 cnviinm 5016 iotanul 5039 funimaexglem 5142 fvelrnb 5401 fvmptssdm 5437 fnfvrnss 5512 fressnfv 5539 fconstfvm 5570 f1mpt 5604 ovprc 5738 fo1stresm 5990 fo2ndresm 5991 spc2ed 6060 opeliunxp2f 6065 reldmtpos 6080 tfrlem5 6141 tfrlem9 6146 tfri2 6193 frecfcllem 6231 frecsuclem 6233 fvmptmap 6509 ixpiinm 6548 ixp0 6555 mptelixpg 6558 ener 6603 domtr 6609 unen 6640 xpf1o 6667 mapen 6669 cardval3ex 6952 distrnqg 7096 nqnq0pi 7147 nqnq0a 7163 nqnq0m 7164 distrnq0 7168 nqprloc 7254 ltexprlemopl 7310 ltexprlemopu 7312 recexre 8206 nn1suc 8597 msqznn 9003 nn0ind 9017 fnn0ind 9019 ublbneg 9255 qreccl 9284 fzo1fzo0n0 9801 elfzom1elp1fzo 9820 fzo0end 9841 fzind2 9857 flqeqceilz 9932 nnsinds 10057 nn0sinds 10058 ser0f 10129 hashfacen 10420 redivap 10487 imdivap 10494 cvg1nlemres 10597 sqrt0 10616 summodclem3 10988 fsump1i 11041 cos1bnd 11264 odd2np1 11365 opoe 11387 omoe 11388 opeo 11389 omeo 11390 dfgcd2 11495 gcdmultiplez 11502 dvdssq 11512 algfx 11526 setsfun0 11777 neipsm 12105 txbas 12208 elcncf1di 12479 bdbm1.3ii 12670 |
Copyright terms: Public domain | W3C validator |