![]() |
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 255 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: mpand 421 mpan2i 423 ralxfrd 4312 rexxfrd 4313 elunirn 5583 onunsnss 6707 xpfi 6720 snon0 6725 genprndl 7177 genprndu 7178 addlsub 7945 letrp1 8406 peano2uz2 8952 uzind 8956 xrre 9386 xrre2 9387 flqge 9838 monoord 10042 facwordi 10279 facavg 10285 dvdsmultr1 11277 ltoddhalfle 11336 dvdsgcdb 11445 dfgcd2 11446 coprmgcdb 11513 coprmdvds2 11518 exprmfct 11562 prmdvdsfz 11563 prmfac1 11574 rpexp 11575 |
Copyright terms: Public domain | W3C validator |