![]() |
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 140 | . 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓)) |
4 | 1, 3 | syl5ib 153 | 1 ⊢ (𝜒 → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl5ibrcom 156 biimprd 157 nbn2 687 limelon 4329 eldifpw 4406 ssonuni 4412 onsucuni2 4487 peano2 4517 limom 4535 elrnmpt1 4798 cnveqb 5002 cnveq0 5003 relcoi1 5078 ndmfvg 5460 ffvresb 5591 caovord3d 5949 poxp 6137 nnm0r 6383 nnacl 6384 nnacom 6388 nnaass 6389 nndi 6390 nnmass 6391 nnmsucr 6392 nnmcom 6393 brecop 6527 ecopovtrn 6534 ecopovtrng 6537 elpm2r 6568 map0g 6590 fundmen 6708 mapxpen 6750 phpm 6767 f1vrnfibi 6841 elfir 6869 mulcmpblnq 7200 ordpipqqs 7206 mulcmpblnq0 7276 genpprecll 7346 genppreclu 7347 addcmpblnr 7571 ax1rid 7709 axpre-mulgt0 7719 cnegexlem1 7961 msqge0 8402 mulge0 8405 ltleap 8418 nnmulcl 8765 nnsub 8783 elnn0z 9091 ztri3or0 9120 nneoor 9177 uz11 9372 xltnegi 9648 frec2uzuzd 10206 seq3fveq2 10273 seq3shft2 10277 seq3split 10283 seq3caopr3 10285 seq3id2 10313 seq3homo 10314 m1expcl2 10346 expadd 10366 expmul 10369 faclbnd 10519 hashfzp1 10602 hashfacen 10611 seq3coll 10617 caucvgrelemcau 10784 recan 10913 rexanre 11024 fsumiun 11278 efexp 11425 dvdstr 11566 alzdvds 11588 zob 11624 gcdmultiplez 11745 dvdssq 11755 cncongr2 11821 elrestr 12167 restopn2 12391 txcn 12483 txlm 12487 isxms2 12660 bj-om 13306 bj-inf2vnlem2 13340 bj-inf2vn 13343 bj-inf2vn2 13344 |
Copyright terms: Public domain | W3C validator |