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 691 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mp2ani 694 wfi 6175 ordelinel 6283 dif20el 8121 domunfican 8780 mulgt1 11488 recgt1i 11526 recreclt 11528 ledivp1i 11554 nngt0 11657 nnrecgt0 11669 elnnnn0c 11931 elnnz1 11997 recnz 12046 uz3m2nn 12280 ledivge1le 12450 xrub 12695 1mod 13261 expubnd 13531 expnbnd 13583 expnlbnd 13584 hashgt23el 13775 resqrex 14600 sin02gt0 15535 oddge22np1 15688 dvdsnprmd 16024 prmlem1 16431 prmlem2 16443 lsmss2 18724 ovolicopnf 24054 voliunlem3 24082 volsup 24086 volivth 24137 itg2seq 24272 itg2monolem2 24281 reeff1olem 24963 sinq12gt0 25022 logdivlti 25130 logdivlt 25131 efexple 25785 gausslemma2dlem4 25873 axlowdimlem16 26671 axlowdimlem17 26672 axlowdim 26675 rusgr1vtx 27298 dmdbr2 30008 dfon2lem3 32928 dfon2lem7 32932 frpoind 32978 frind 32983 nn0prpwlem 33568 bj-resta 34282 tan2h 34766 mblfinlem4 34814 m1mod0mod1 43410 iccpartgt 43434 gbegt5 43773 gbowgt5 43774 sbgoldbalt 43793 sgoldbeven3prm 43795 nnsum4primesodd 43808 nnsum4primesoddALTV 43809 evengpoap3 43811 nnsum4primesevenALTV 43813 m1modmmod 44479 difmodm1lt 44480 regt1loggt0 44494 rege1logbrege0 44516 rege1logbzge0 44517 |
Copyright terms: Public domain | W3C validator |