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 1113 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 1125 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 1115 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3com12 1125 sotri3 6009 isinf 8915 infssuni 8991 fin1a2lem10 10047 elfz1b 13205 bernneq 13820 expnngt1 13832 swrdco 14426 dfgcd2 16130 lmodvsmmulgdi 19958 mamufacex 21312 gausslemma2dlem1a 26270 upgrewlkle2 27718 pthdivtx 27840 clwwlkinwwlk 28147 upgr3v3e3cycl 28287 upgr4cycl4dv4e 28292 numclwwlk2lem1lem 28449 frgrregord013 28502 ssltun1 33765 ssltright 33818 ax6e2ndeqALT 42252 fmtnofac2 44722 |
Copyright terms: Public domain | W3C validator |