Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imp2 | Structured version Visualization version GIF version |
Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3imp1.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
3imp2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp1.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | 3impd 1340 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | imp 407 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: wereu 5545 ovg 7302 fisup2g 8921 fiinf2g 8953 cfcoflem 9683 ttukeylem5 9924 dedekindle 10793 grplcan 18101 mulgnnass 18202 dmdprdsplit2 19099 mulgass2 19282 lmodvsdi 19588 lmodvsdir 19589 lmodvsass 19590 lss1d 19666 islmhm2 19741 lspsolvlem 19845 lbsextlem2 19862 cygznlem2a 20644 isphld 20728 t0dist 21863 hausnei 21866 nrmsep3 21893 fclsopni 22553 fcfneii 22575 ax5seglem5 26647 axcont 26690 grporcan 28223 grpolcan 28235 slmdvsdi 30771 slmdvsdir 30772 slmdvsass 30773 mclsppslem 32728 broutsideof2 33481 poimirlem31 34805 broucube 34808 frinfm 34893 crngm23 35163 pridl 35198 pridlc 35232 dmnnzd 35236 dmncan1 35237 paddasslem5 36842 or2expropbi 43150 sfprmdvdsmersenne 43615 |
Copyright terms: Public domain | W3C validator |