New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > syl5ib | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5ib.1 | ⊢ (φ → ψ) |
syl5ib.2 | ⊢ (χ → (ψ ↔ θ)) |
Ref | Expression |
---|---|
syl5ib | ⊢ (χ → (φ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ib.1 | . 2 ⊢ (φ → ψ) | |
2 | syl5ib.2 | . . 3 ⊢ (χ → (ψ ↔ θ)) | |
3 | 2 | biimpd 198 | . 2 ⊢ (χ → (ψ → θ)) |
4 | 1, 3 | syl5 28 | 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: syl5ibcom 211 syl5ibr 212 19.23tOLD 1819 nfsb4t 2080 ax11indalem 2197 ax11inda2ALT 2198 gencl 2887 spsbc 3058 eqsbc3r 3103 ssnelpss 3613 adj11 3889 uniintsn 3963 phi011lem1 4598 optocl 4838 xpexr 5109 funimass1 5169 fneu 5187 dmfex 5247 fniniseg 5371 eqfnfv 5392 eqfnfv2 5393 elpreima 5407 fnasrn 5417 dffo4 5423 fconst5 5455 funiunfv 5467 dff13 5471 f1ocnvfv 5478 f1ocnvfvb 5479 ce0ncpw1 6185 cecl 6186 dflec3 6221 lenc 6223 |
Copyright terms: Public domain | W3C validator |