Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpan2d | Unicode version |
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
mpan2d.1 | |
mpan2d.2 |
Ref | Expression |
---|---|
mpan2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpan2d.1 | . 2 | |
2 | mpan2d.2 | . . 3 | |
3 | 2 | expd 256 | . 2 |
4 | 1, 3 | mpid 42 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: mpand 427 mpan2i 429 ralxfrd 4447 rexxfrd 4448 elunirn 5745 onunsnss 6894 xpfi 6907 snon0 6913 genprndl 7483 genprndu 7484 addlsub 8289 letrp1 8764 peano2uz2 9319 uzind 9323 xrre 9777 xrre2 9778 flqge 10238 monoord 10432 facwordi 10674 facavg 10680 dvdsmultr1 11793 ltoddhalfle 11852 dvdsgcdb 11968 dfgcd2 11969 coprmgcdb 12042 coprmdvds2 12047 exprmfct 12092 prmdvdsfz 12093 prmfac1 12106 rpexp 12107 eulerthlemh 12185 pcpremul 12247 pcdvdsb 12273 pcprmpw2 12286 pockthlem 12308 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |