![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an1 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an1.1 | ⊢ 𝜑 |
mp3an1.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an1 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an1.1 | . 2 ⊢ 𝜑 | |
2 | mp3an1.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expb 1140 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
4 | 1, 3 | mpan 415 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: mp3an12 1259 mp3an1i 1262 mp3anl1 1263 mp3an 1269 mp3an2i 1274 mp3an3an 1275 tfrlem9 5968 rdgexgg 6027 oaexg 6092 omexg 6095 oeiexg 6097 oav2 6107 nnaordex 6166 mulidnq 6641 1idpru 6843 addgt0sr 7014 muladd11 7308 cnegex 7353 negsubdi 7431 renegcl 7436 mulneg1 7566 ltaddpos 7623 addge01 7643 rimul 7752 recclap 7834 recidap 7841 recidap2 7842 recdivap2 7880 divdiv23apzi 7920 ltmul12a 8005 lemul12a 8007 mulgt1 8008 ltmulgt11 8009 gt0div 8015 ge0div 8016 ltdiv23i 8071 8th4div3 8317 gtndiv 8523 nn0ind 8542 fnn0ind 8544 xrre2 8964 ioorebasg 9074 fzen 9138 elfz0ubfz0 9213 expubnd 9630 le2sq2 9648 bernneq 9690 expnbnd 9693 faclbnd6 9768 bccl 9791 shftfval 9847 mulreap 9889 caucvgrelemrec 10003 odd2np1 10417 opoe 10439 omoe 10440 opeo 10441 omeo 10442 gcdadd 10520 gcdmultiple 10553 algcvgblem 10575 ialgcvga 10577 isprm3 10644 coprm 10667 |
Copyright terms: Public domain | W3C validator |