![]() |
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 516 | . 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓)) |
3 | mpanl1.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 572 | 1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: mpanl12 690 frc 5369 oeoelem 8023 ercnv 8108 frfi 8556 fin23lem23 9544 divdiv23zi 11192 recp1lt1 11337 divgt0i 11347 divge0i 11348 ltreci 11349 lereci 11350 lt2msqi 11351 le2msqi 11352 msq11i 11353 ltdiv23i 11363 fnn0ind 11892 elfzp1b 12798 elfzm1b 12799 sqrt11i 14603 sqrtmuli 14604 sqrtmsq2i 14606 sqrtlei 14607 sqrtlti 14608 fsum 14935 fprod 15153 blometi 28372 spansnm0i 29223 lnopli 29541 lnfnli 29613 opsqrlem1 29713 opsqrlem6 29718 mdslmd3i 29905 atordi 29957 mdsymlem1 29976 gsummpt2co 30555 finxpreclem4 34153 ptrecube 34370 fdc 34499 prter3 35500 |
Copyright terms: Public domain | W3C validator |