| 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 258 |
. 2
|
| 4 | 1, 3 | mpid 42 |
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-ia3 108 |
| This theorem is referenced by: mpand 429 mpan2i 431 ralxfrd 4509 rexxfrd 4510 elunirn 5835 onunsnss 7014 xpfi 7029 snon0 7037 genprndl 7634 genprndu 7635 addlsub 8442 letrp1 8921 peano2uz2 9480 uzind 9484 xrre 9942 xrre2 9943 flqge 10425 monoord 10630 facwordi 10885 facavg 10891 dvdsmultr1 12142 ltoddhalfle 12204 dvdsgcdb 12334 dfgcd2 12335 coprmgcdb 12410 coprmdvds2 12415 exprmfct 12460 prmdvdsfz 12461 prmfac1 12474 rpexp 12475 eulerthlemh 12553 pcpremul 12616 pcdvdsb 12643 pcprmpw2 12656 pockthlem 12679 4sqlem11 12724 lgsne0 15515 gausslemma2dlem1a 15535 gausslemma2dlem2 15539 lgseisenlem1 15547 lgseisenlem2 15548 lgsquadlem1 15554 lgsquadlem2 15555 lgsquadlem3 15556 lgsquad2lem1 15558 lgsquad2lem2 15559 |
| Copyright terms: Public domain | W3C validator |