![]() |
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 1110 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 1122 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 1112 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: 3com12 1122 sotri3 6153 isinf 9294 isinfOLD 9295 infssuni 9384 fin1a2lem10 10447 elfz1b 13630 bernneq 14265 expnngt1 14277 swrdco 14873 dfgcd2 16580 lmodvsmmulgdi 20912 mamufacex 22416 gausslemma2dlem1a 27424 ssltun1 27868 ssltright 27925 expsgt0 28430 upgrewlkle2 29639 pthdivtx 29762 clwwlkinwwlk 30069 upgr3v3e3cycl 30209 upgr4cycl4dv4e 30214 numclwwlk2lem1lem 30371 frgrregord013 30424 ax6e2ndeqALT 44929 fmtnofac2 47494 |
Copyright terms: Public domain | W3C validator |