![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpanl1 | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
Ref | Expression |
---|---|
mpanl1.1 | ⊢ 𝜑 |
mpanl1.2 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpanl1 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpanl1.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | jctl 523 | . 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓)) |
3 | mpanl1.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 579 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 396 |
This theorem is referenced by: mpanl12 699 frc 5633 oeoelem 8594 ercnv 8721 frfi 9285 fin23lem23 10318 divdiv23zi 11965 recp1lt1 12110 divgt0i 12120 divge0i 12121 ltreci 12122 lereci 12123 lt2msqi 12124 le2msqi 12125 msq11i 12126 ltdiv23i 12136 fnn0ind 12659 elfzp1b 13576 elfzm1b 13577 sqrt11i 15329 sqrtmuli 15330 sqrtmsq2i 15332 sqrtlei 15333 sqrtlti 15334 fsum 15664 fprod 15883 blometi 30528 spansnm0i 31375 lnopli 31693 lnfnli 31765 opsqrlem1 31865 opsqrlem6 31870 mdslmd3i 32057 atordi 32109 mdsymlem1 32128 gsummpt2co 32671 finxpreclem4 36766 ptrecube 36982 fdc 37107 prter3 38246 |
Copyright terms: Public domain | W3C validator |