| 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 1349 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
| 3 | 2 | imp 406 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: wereu 5681 ovg 7598 fisup2g 9508 fiinf2g 9540 cfcoflem 10312 ttukeylem5 10553 dedekindle 11425 grplcan 19018 mulgnnass 19127 dmdprdsplit2 20066 mulgass2 20306 lmodvsdi 20883 lmodvsdir 20884 lmodvsass 20885 lss1d 20961 islmhm2 21037 lspsolvlem 21144 lbsextlem2 21161 cygznlem2a 21586 isphld 21672 t0dist 23333 hausnei 23336 nrmsep3 23363 fclsopni 24023 fcfneii 24045 ax5seglem5 28948 axcont 28991 grporcan 30537 grpolcan 30549 slmdvsdi 33221 slmdvsdir 33222 slmdvsass 33223 elrspunidl 33456 zarcmplem 33880 mclsppslem 35588 broutsideof2 36123 poimirlem31 37658 broucube 37661 frinfm 37742 crngm23 38009 pridl 38044 pridlc 38078 dmnnzd 38082 dmncan1 38083 paddasslem5 39826 or2expropbi 47046 elsetpreimafveqfv 47379 sfprmdvdsmersenne 47590 isgrtri 47910 |
| Copyright terms: Public domain | W3C validator |