New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 197 | . 2 ⊢ (φ → ψ) |
3 | sylbir.2 | . 2 ⊢ (ψ → χ) | |
4 | 2, 3 | syl 15 | 1 ⊢ (φ → χ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 |
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 177 |
This theorem is referenced by: 3imtr3i 256 ex 423 3ori 1242 19.38 1794 ax12olem5 1931 sbi2 2064 sb5rf 2090 ax11eq 2193 ax11el 2194 mo 2226 mo2 2233 2mo 2282 axie2 2329 bm1.1 2338 necon1i 2560 sbhypf 2904 vtocl2 2910 vtocl3 2911 reu6 3025 uneqin 3506 inelcm 3605 difin0ss 3616 difprsn1 3847 unissint 3950 intminss 3952 iununi 4050 pw10b 4166 iotanul 4354 peano5 4409 elsuci 4414 nndisjeq 4429 nnceleq 4430 tfin11 4493 sfinltfin 4535 copsex2g 4609 opelopabsb 4697 opelopabt 4699 opelrn 4961 elimasn 5019 xpnz 5045 ssxpb 5055 funcnvres2 5167 tz6.12 5345 fnfvrnss 5429 fressnfv 5439 fconst5 5455 fconstfv 5456 ovidig 5593 ovres 5602 ovconst2 5611 oprssdm 5612 ndmovcl 5614 fvfullfun 5864 ecopqsi 5981 ncaddccl 6144 nceleq 6149 dflec3 6221 lenc 6223 letc 6231 |
Copyright terms: Public domain | W3C validator |