![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imp | Unicode version |
Description: Importation inference. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3imp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3imp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3imp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | imp31 256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylbi 121 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3impa 1194 3imp31 1196 3imp231 1197 3impb 1199 3impia 1200 3impib 1201 3com23 1209 3an1rs 1219 3imp1 1220 3impd 1221 syl3an2 1272 syl3an3 1273 3jao 1301 biimp3ar 1346 poxp 6230 tfrlemibxssdm 6325 tfr1onlembxssdm 6341 tfrcllembxssdm 6354 nndi 6484 nnmass 6485 pr2nelem 7187 xnn0lenn0nn0 9861 difelfzle 10129 fzo1fzo0n0 10178 elfzo0z 10179 fzofzim 10183 elfzodifsumelfzo 10196 mulexp 10554 expadd 10557 expmul 10560 bernneq 10635 facdiv 10711 addmodlteqALT 11857 ltoddhalfle 11890 halfleoddlt 11891 dfgcd2 12007 cncongr1 12095 oddprmgt2 12126 prmfac1 12144 infpnlem1 12349 dfgrp3me 12902 mulgaddcom 12938 mulginvcom 12939 fiinopn 13373 opnneissb 13526 blssps 13798 blss 13799 2sqlem10 14332 |
Copyright terms: Public domain | W3C validator |