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 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 425 mpan2i 427 ralxfrd 4353 rexxfrd 4354 elunirn 5635 onunsnss 6773 xpfi 6786 snon0 6792 genprndl 7297 genprndu 7298 addlsub 8100 letrp1 8574 peano2uz2 9126 uzind 9130 xrre 9571 xrre2 9572 flqge 10023 monoord 10217 facwordi 10454 facavg 10460 dvdsmultr1 11458 ltoddhalfle 11517 dvdsgcdb 11628 dfgcd2 11629 coprmgcdb 11696 coprmdvds2 11701 exprmfct 11745 prmdvdsfz 11746 prmfac1 11757 rpexp 11758 |
Copyright terms: Public domain | W3C validator |