![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5ibr | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.) |
Ref | Expression |
---|---|
syl5ibr.1 | ⊢ (φ → θ) |
syl5ibr.2 | ⊢ (χ → (ψ ↔ θ)) |
Ref | Expression |
---|---|
syl5ibr | ⊢ (χ → (φ → ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ibr.1 | . 2 ⊢ (φ → θ) | |
2 | syl5ibr.2 | . . 3 ⊢ (χ → (ψ ↔ θ)) | |
3 | 2 | bicomd 129 | . 2 ⊢ (χ → (θ ↔ ψ)) |
4 | 1, 3 | syl5ib 143 | 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: syl5ibrcom 146 biimprd 147 nbn2 612 limelon 4102 eldifpw 4174 ssonuni 4180 peano2 4261 limom 4279 elrnmpt1 4528 cnveqb 4719 cnveq0 4720 relcoi1 4792 ndmfvg 5147 ffvresb 5271 caovord3d 5613 poxp 5794 nnm0r 5997 nnacl 5998 nnacom 6002 nnaass 6003 nndi 6004 nnmass 6005 nnmsucr 6006 nnmcom 6007 brecop 6132 ecopovtrn 6139 ecopovtrng 6142 fundmen 6222 mulcmpblnq 6352 ordpipqqs 6358 mulcmpblnq0 6427 genpprecll 6497 genppreclu 6498 addcmpblnr 6667 ax1rid 6761 axpre-mulgt0 6771 cnegexlem1 6983 msqge0 7400 mulge0 7403 ltleap 7413 nnmulcl 7716 nnsub 7733 elnn0z 8034 ztri3or0 8063 nneoor 8116 uz11 8271 xltnegi 8518 frec2uzuzd 8869 iseqfveq2 8905 m1expcl2 8931 expadd 8951 expmul 8954 bj-om 9396 peano5setOLD 9400 bj-inf2vnlem2 9431 bj-inf2vn 9434 bj-inf2vn2 9435 |
Copyright terms: Public domain | W3C validator |