| 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 580 | 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 207 df-an 396 |
| This theorem is referenced by: mpanl12 702 frc 5648 oeoelem 8636 ercnv 8766 frfi 9321 fin23lem23 10366 divdiv23zi 12020 recp1lt1 12166 divgt0i 12176 divge0i 12177 ltreci 12178 lereci 12179 lt2msqi 12180 le2msqi 12181 msq11i 12182 ltdiv23i 12192 fnn0ind 12717 elfzp1b 13641 elfzm1b 13642 sqrt11i 15423 sqrtmuli 15424 sqrtmsq2i 15426 sqrtlei 15427 sqrtlti 15428 fsum 15756 fprod 15977 blometi 30822 spansnm0i 31669 lnopli 31987 lnfnli 32059 opsqrlem1 32159 opsqrlem6 32164 mdslmd3i 32351 atordi 32403 mdsymlem1 32422 gsummpt2co 33051 finxpreclem4 37395 ptrecube 37627 fdc 37752 prter3 38883 |
| Copyright terms: Public domain | W3C validator |