![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpan2d | GIF 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: → wi 4 ∧ wa 104 |
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 4480 rexxfrd 4481 elunirn 5788 onunsnss 6946 xpfi 6959 snon0 6966 genprndl 7551 genprndu 7552 addlsub 8358 letrp1 8836 peano2uz2 9391 uzind 9395 xrre 9852 xrre2 9853 flqge 10315 monoord 10509 facwordi 10755 facavg 10761 dvdsmultr1 11873 ltoddhalfle 11933 dvdsgcdb 12049 dfgcd2 12050 coprmgcdb 12123 coprmdvds2 12128 exprmfct 12173 prmdvdsfz 12174 prmfac1 12187 rpexp 12188 eulerthlemh 12266 pcpremul 12328 pcdvdsb 12355 pcprmpw2 12368 pockthlem 12391 4sqlem11 12436 lgsne0 14917 lgseisenlem1 14928 lgseisenlem2 14929 |
Copyright terms: Public domain | W3C validator |