![]() |
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 1123 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3com12 1123 sotri3 6131 isinf 9259 isinfOLD 9260 infssuni 9342 fin1a2lem10 10403 elfz1b 13569 bernneq 14191 expnngt1 14203 swrdco 14787 dfgcd2 16487 lmodvsmmulgdi 20506 mamufacex 21890 gausslemma2dlem1a 26865 ssltun1 27306 ssltright 27363 upgrewlkle2 28860 pthdivtx 28983 clwwlkinwwlk 29290 upgr3v3e3cycl 29430 upgr4cycl4dv4e 29435 numclwwlk2lem1lem 29592 frgrregord013 29645 ax6e2ndeqALT 43682 fmtnofac2 46227 |
Copyright terms: Public domain | W3C validator |