![]() |
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 1112 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 1114 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: 3com12 1124 sotri3 6088 isinf 9210 isinfOLD 9211 infssuni 9293 fin1a2lem10 10353 elfz1b 13519 bernneq 14141 expnngt1 14153 swrdco 14735 dfgcd2 16435 lmodvsmmulgdi 20401 mamufacex 21761 gausslemma2dlem1a 26736 ssltun1 27176 ssltright 27230 upgrewlkle2 28603 pthdivtx 28726 clwwlkinwwlk 29033 upgr3v3e3cycl 29173 upgr4cycl4dv4e 29178 numclwwlk2lem1lem 29335 frgrregord013 29388 ax6e2ndeqALT 43305 fmtnofac2 45851 |
Copyright terms: Public domain | W3C validator |