![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impib | Unicode version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impib.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3impib |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impib.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | expd 258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3imp 1193 |
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 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: mob 2919 eqreu 2929 iotam 5208 funimaexglem 5299 ssimaexg 5578 rbropap 6243 dfsmo2 6287 3ecoptocl 6623 distrnq0 7457 addassnq0 7460 uzind 9362 fzind 9366 fnn0ind 9367 xltnegi 9833 facwordi 10715 shftvalg 10840 shftval4g 10841 mulgcd 12011 coprmdvds1 12085 pcfac 12342 mgmcl 12772 mhmlin 12852 mhmmulg 13017 issubg2m 13042 nsgbi 13057 srgmulgass 13165 dvdsrtr 13263 issubrg2 13362 inopn 13434 basis1 13478 cnmpt2t 13724 cnmpt22 13725 cnmptcom 13729 xmeteq0 13790 sincosq1sgn 14178 sincosq2sgn 14179 sincosq3sgn 14180 sincosq4sgn 14181 speano5 14616 |
Copyright terms: Public domain | W3C validator |