![]() |
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 707 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: mp2ani 710 wfi 5630 ordelinel 5742 ordelinelOLD 5743 dif20el 7472 domunfican 8118 mulgt1 10761 recgt1i 10799 recreclt 10801 ledivp1i 10828 nngt0 10926 nnrecgt0 10935 elnnnn0c 11215 elnnz1 11280 recnz 11328 uz3m2nn 11607 ledivge1le 11777 xrub 12014 1mod 12564 expubnd 12783 expnbnd 12855 expnlbnd 12856 resqrex 13839 sin02gt0 14761 oddge22np1 14911 dvdsnprmd 15241 prmlem1 15652 prmlem2 15665 lsmss2 17904 ovolicopnf 23099 voliunlem3 23127 volsup 23131 volivth 23181 itg2seq 23315 itg2monolem2 23324 reeff1olem 24004 sinq12gt0 24063 logdivlti 24170 logdivlt 24171 efexple 24806 gausslemma2dlem4 24894 axlowdimlem16 25637 axlowdimlem17 25638 axlowdim 25641 dmdbr2 28546 dfon2lem3 30934 dfon2lem7 30938 frind 30984 nn0prpwlem 31487 bj-resta 32230 tan2h 32571 mblfinlem4 32619 m1mod0mod1 39949 iccpartgt 39965 gbegt5 40183 gbogt5 40184 sgoldbalt 40203 nnsum4primesodd 40212 nnsum4primesoddALTV 40213 evengpoap3 40215 nnsum4primesevenALTV 40217 pfx2 40275 rusgr1vtx 40788 frgrwopreglem2 41482 m1modmmod 42110 difmodm1lt 42111 regt1loggt0 42128 rege1logbrege0 42150 rege1logbzge0 42151 |
Copyright terms: Public domain | W3C validator |