| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3imp21 | Structured version Visualization version GIF version | ||
| Description: The importation inference 3imp 1111 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1124 by Wolf Lammen, 23-Jun-2022.) |
| Ref | Expression |
|---|---|
| 3imp.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| Ref | Expression |
|---|---|
| 3imp21 | ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3imp.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
| 2 | 1 | com13 88 | . 2 ⊢ (𝜒 → (𝜓 → (𝜑 → 𝜃))) |
| 3 | 2 | 3imp231 1113 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 df-3an 1089 |
| This theorem is referenced by: 3com12 1124 sotri3 6150 isinf 9296 isinfOLD 9297 infssuni 9386 fin1a2lem10 10449 elfz1b 13633 bernneq 14268 expnngt1 14280 swrdco 14876 dfgcd2 16583 lmodvsmmulgdi 20895 mamufacex 22400 gausslemma2dlem1a 27409 ssltun1 27853 ssltright 27910 expsgt0 28415 upgrewlkle2 29624 pthdivtx 29747 clwwlkinwwlk 30059 upgr3v3e3cycl 30199 upgr4cycl4dv4e 30204 numclwwlk2lem1lem 30361 frgrregord013 30414 ax6e2ndeqALT 44951 fmtnofac2 47556 |
| Copyright terms: Public domain | W3C validator |