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 949 | . 2 | |
2 | 3imp.1 | . . 3 | |
3 | 2 | imp31 254 | . 2 |
4 | 1, 3 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: 3impa 1161 3impb 1162 3impia 1163 3impib 1164 3com23 1172 3an1rs 1182 3imp1 1183 3impd 1184 syl3an2 1235 syl3an3 1236 3jao 1264 biimp3ar 1309 poxp 6097 tfrlemibxssdm 6192 tfr1onlembxssdm 6208 tfrcllembxssdm 6221 nndi 6350 nnmass 6351 pr2nelem 7015 xnn0lenn0nn0 9616 difelfzle 9879 fzo1fzo0n0 9928 elfzo0z 9929 fzofzim 9933 elfzodifsumelfzo 9946 mulexp 10300 expadd 10303 expmul 10306 bernneq 10380 facdiv 10452 addmodlteqALT 11484 ltoddhalfle 11517 halfleoddlt 11518 dfgcd2 11629 cncongr1 11711 oddprmgt2 11741 prmfac1 11757 fiinopn 12098 opnneissb 12251 blssps 12523 blss 12524 |
Copyright terms: Public domain | W3C validator |