| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpani | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
| Ref | Expression |
|---|---|
| mpani.1 | ⊢ 𝜓 |
| mpani.2 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
| Ref | Expression |
|---|---|
| mpani | ⊢ (𝜑 → (𝜒 → 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpani.1 | . . 3 ⊢ 𝜓 | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 𝜓) |
| 3 | mpani.2 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
| 4 | 2, 3 | mpand 695 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: mp2ani 698 frpoind 6363 wfiOLD 6372 ordelinel 6485 dif20el 8543 domunfican 9361 frind 9790 mulgt1OLD 12126 recgt1i 12165 recreclt 12167 ledivp1i 12193 nngt0 12297 nnrecgt0 12309 elnnnn0c 12571 elnnz1 12643 recnz 12693 uz3m2nn 12933 ledivge1le 13106 xrub 13354 1mod 13943 expubnd 14217 expnbnd 14271 expnlbnd 14272 hashgt23el 14463 resqrex 15289 sin02gt0 16228 oddge22np1 16386 dvdsnprmd 16727 prmlem1 17145 prmlem2 17157 lsmss2 19685 ovolicopnf 25559 voliunlem3 25587 volsup 25591 volivth 25642 itg2seq 25777 itg2monolem2 25786 reeff1olem 26490 sinq12gt0 26549 logdivlti 26662 logdivlt 26663 efexple 27325 gausslemma2dlem4 27413 axlowdimlem16 28972 axlowdimlem17 28973 axlowdim 28976 rusgr1vtx 29606 dmdbr2 32322 dfon2lem3 35786 dfon2lem7 35790 nn0prpwlem 36323 bj-resta 37097 tan2h 37619 mblfinlem4 37667 m1mod0mod1 47356 iccpartgt 47414 gbegt5 47748 gbowgt5 47749 sbgoldbalt 47768 sgoldbeven3prm 47770 nnsum4primesodd 47783 nnsum4primesoddALTV 47784 evengpoap3 47786 nnsum4primesevenALTV 47788 m1modmmod 48442 difmodm1lt 48443 regt1loggt0 48457 rege1logbrege0 48479 rege1logbzge0 48480 |
| Copyright terms: Public domain | W3C validator |