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 1107 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 1119 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 1109 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: 3com12 1119 sotri3 5990 isinf 8731 infssuni 8815 fin1a2lem10 9831 elfz1b 12977 bernneq 13591 expnngt1 13603 swrdco 14199 dfgcd2 15894 lmodvsmmulgdi 19669 mamufacex 21000 gausslemma2dlem1a 25941 upgrewlkle2 27388 pthdivtx 27510 clwwlkinwwlk 27818 upgr3v3e3cycl 27959 upgr4cycl4dv4e 27964 numclwwlk2lem1lem 28121 frgrregord013 28174 ax6e2ndeqALT 41285 fmtnofac2 43751 |
Copyright terms: Public domain | W3C validator |