Theorem impl 459

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
impl.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
impl	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem impl

Step	Hyp	Ref	Expression
1		impl.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 419	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 421	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  sbc2iedv  3821  csbie2t  3891  frinxp  5731  ordelord  6369  foco2  7091  f1ounsn  7257  frxp  8107  mpocurryd  8250  omsmolem  8628  erth  8734  unblem1  9237  unwdomg  9533  cflim2  10221  distrlem1pr  10984  uz11  12865  elpq  12977  xmulge0  13288  max0add  15338  lcmfunsnlem2lem1  16673  divgcdcoprm0  16700  cncongr1  16702  prmpwdvds  16941  imasleval  17572  issgrpd  18765  dfgrp3lem  19081  resscntz  19374  ablfac1c  20114  lbsind  21148  isphld  21707  mplcoe5lem  22093  cply1mul  22360  smadiadetr  22736  chfacfisf  22915  chfacfisfcpmat  22916  chcoeffeq  22947  cayhamlem3  22948  tx1stc  23711  ioorcl  25640  coemullem  26311  xrlimcnp  27034  fsumdvdscom  27250  fsumvma  27278  cusgrres  29650  usgredgsscusgredg  29661  clwlkclwwlklem2a  30201  clwwlkext2edg  30259  frgrwopreglem5ALT  30525  frgr2wwlkeu  30530  frgr2wwlk1  30532  grpoidinvlem3  30710  htthlem  31121  atcvat4i  32601  abfmpeld  32857  ressupprn  32893  isarchi3  33368  qsidomlem2  33641  ordtconnlem1  34222  gonarlem  35745  fmlasucdisj  35750  funpartfun  36294  relowlssretop  37858  ltflcei  38108  neificl  38253  keridl  38532  eqvrelth  39195  cvrat4  40068  ps-2  40103  mpaaeu  43728  clcnvlem  44200  fcoresf1  47664  modlt0b  47964  iccpartiltu  48029  2pwp1prm  48199  bgoldbtbnd  48432  isuspgrimlem  48518  grimedg  48558  grimgrtri  48572  lmod0rng  48852  lincext1  49077