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 1350 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | imp 410 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: wereu 5544 ovg 7370 fisup2g 9081 fiinf2g 9113 cfcoflem 9883 ttukeylem5 10124 dedekindle 10993 grplcan 18422 mulgnnass 18523 dmdprdsplit2 19430 mulgass2 19616 lmodvsdi 19919 lmodvsdir 19920 lmodvsass 19921 lss1d 19997 islmhm2 20072 lspsolvlem 20176 lbsextlem2 20193 cygznlem2a 20529 isphld 20613 t0dist 22219 hausnei 22222 nrmsep3 22249 fclsopni 22909 fcfneii 22931 ax5seglem5 27021 axcont 27064 grporcan 28596 grpolcan 28608 slmdvsdi 31184 slmdvsdir 31185 slmdvsass 31186 elrspunidl 31317 zarcmplem 31542 mclsppslem 33255 broutsideof2 34158 poimirlem31 35543 broucube 35546 frinfm 35628 crngm23 35895 pridl 35930 pridlc 35964 dmnnzd 35968 dmncan1 35969 paddasslem5 37573 or2expropbi 44198 elsetpreimafveqfv 44515 sfprmdvdsmersenne 44726 |
Copyright terms: Public domain | W3C validator |