![]() |
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 1109 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 1121 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 1111 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1085 |
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 395 df-3an 1087 |
This theorem is referenced by: 3com12 1121 sotri3 6130 isinf 9262 isinfOLD 9263 infssuni 9345 fin1a2lem10 10406 elfz1b 13574 bernneq 14196 expnngt1 14208 swrdco 14792 dfgcd2 16492 lmodvsmmulgdi 20651 mamufacex 22111 gausslemma2dlem1a 27104 ssltun1 27546 ssltright 27603 upgrewlkle2 29130 pthdivtx 29253 clwwlkinwwlk 29560 upgr3v3e3cycl 29700 upgr4cycl4dv4e 29705 numclwwlk2lem1lem 29862 frgrregord013 29915 ax6e2ndeqALT 43994 fmtnofac2 46535 |
Copyright terms: Public domain | W3C validator |