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 5544 ovg 7302 fisup2g 8920 fiinf2g 8952 cfcoflem 9682 ttukeylem5 9923 dedekindle 10792 grplcan 18099 mulgnnass 18200 dmdprdsplit2 19097 mulgass2 19280 lmodvsdi 19586 lmodvsdir 19587 lmodvsass 19588 lss1d 19664 islmhm2 19739 lspsolvlem 19843 lbsextlem2 19860 cygznlem2a 20642 isphld 20726 t0dist 21861 hausnei 21864 nrmsep3 21891 fclsopni 22551 fcfneii 22573 ax5seglem5 26646 axcont 26689 grporcan 28222 grpolcan 28234 slmdvsdi 30770 slmdvsdir 30771 slmdvsass 30772 mclsppslem 32727 broutsideof2 33480 poimirlem31 34804 broucube 34807 frinfm 34891 crngm23 35161 pridl 35196 pridlc 35230 dmnnzd 35234 dmncan1 35235 paddasslem5 36840 or2expropbi 43146 elsetpreimafveqfv 43429 sfprmdvdsmersenne 43645 |
Copyright terms: Public domain | W3C validator |