![]() |
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 694 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: mp2ani 697 frpoind 6340 wfiOLD 6349 ordelinel 6462 dif20el 8500 domunfican 9316 frind 9741 mulgt1 12069 recgt1i 12107 recreclt 12109 ledivp1i 12135 nngt0 12239 nnrecgt0 12251 elnnnn0c 12513 elnnz1 12584 recnz 12633 uz3m2nn 12871 ledivge1le 13041 xrub 13287 1mod 13864 expubnd 14138 expnbnd 14191 expnlbnd 14192 hashgt23el 14380 resqrex 15193 sin02gt0 16131 oddge22np1 16288 dvdsnprmd 16623 prmlem1 17037 prmlem2 17049 lsmss2 19528 ovolicopnf 25023 voliunlem3 25051 volsup 25055 volivth 25106 itg2seq 25242 itg2monolem2 25251 reeff1olem 25940 sinq12gt0 25999 logdivlti 26110 logdivlt 26111 efexple 26764 gausslemma2dlem4 26852 axlowdimlem16 28195 axlowdimlem17 28196 axlowdim 28199 rusgr1vtx 28825 dmdbr2 31534 dfon2lem3 34695 dfon2lem7 34699 nn0prpwlem 35145 bj-resta 35915 tan2h 36418 mblfinlem4 36466 m1mod0mod1 45972 iccpartgt 46030 gbegt5 46364 gbowgt5 46365 sbgoldbalt 46384 sgoldbeven3prm 46386 nnsum4primesodd 46399 nnsum4primesoddALTV 46400 evengpoap3 46402 nnsum4primesevenALTV 46404 m1modmmod 47109 difmodm1lt 47110 regt1loggt0 47124 rege1logbrege0 47146 rege1logbzge0 47147 |
Copyright terms: Public domain | W3C validator |