Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mp3an12.1 | ⊢ 𝜑 |
mp3an12.2 | ⊢ 𝜓 |
mp3an12.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12.2 | . 2 ⊢ 𝜓 | |
2 | mp3an12.1 | . . 3 ⊢ 𝜑 | |
3 | mp3an12.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an1 1219 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 400 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: ceqsralv 2585 brelrn 4567 funpr 4951 ener 6259 ltaddnq 6505 ltadd1sr 6861 mul02 7384 ltapi 7625 div0ap 7679 divclapzi 7723 divcanap1zi 7724 divcanap2zi 7725 divrecapzi 7726 divcanap3zi 7727 divcanap4zi 7728 divassapzi 7738 divmulapzi 7739 divdirapzi 7740 redivclapzi 7754 ltm1 7812 mulgt1 7829 recgt1i 7864 recreclt 7866 ltmul1i 7886 ltdiv1i 7887 ltmuldivi 7888 ltmul2i 7889 lemul1i 7890 lemul2i 7891 cju 7913 nnge1 7937 nngt0 7939 nnrecgt0 7951 elnnnn0c 8227 elnnz1 8268 recnz 8333 eluzsubi 8500 ge0gtmnf 8736 m1expcl2 9277 1exp 9284 expubnd 9311 expnbnd 9372 expnlbnd 9373 remim 9460 imval2 9494 cjdivapi 9535 absdivapzi 9750 |
Copyright terms: Public domain | W3C validator |