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 426 mpan2i 428 ralxfrd 4424 rexxfrd 4425 elunirn 5718 onunsnss 6863 xpfi 6876 snon0 6882 genprndl 7443 genprndu 7444 addlsub 8249 letrp1 8724 peano2uz2 9276 uzind 9280 xrre 9730 xrre2 9731 flqge 10190 monoord 10384 facwordi 10625 facavg 10631 dvdsmultr1 11737 ltoddhalfle 11796 dvdsgcdb 11912 dfgcd2 11913 coprmgcdb 11980 coprmdvds2 11985 exprmfct 12030 prmdvdsfz 12031 prmfac1 12042 rpexp 12043 eulerthlemh 12121 pcpremul 12183 |
Copyright terms: Public domain | W3C validator |