Theorem impl 456

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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 418	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  sbc2iedv  3779  csbie2t  3846  frinxp  5520  ordelord  6088  foco2  6736  frxp  7673  mpocurryd  7786  omsmolem  8130  erth  8188  unblem1  8616  unwdomg  8894  cflim2  9531  distrlem1pr  10293  uz11  12116  elpq  12224  xmulge0  12527  max0add  14504  lcmfunsnlem2lem1  15811  divgcdcoprm0  15838  cncongr1  15840  prmpwdvds  16069  imasleval  16643  dfgrp3lem  17954  resscntz  18203  ablfac1c  18910  lbsind  19542  mplcoe5lem  19935  cply1mul  20145  isphld  20480  smadiadetr  20968  chfacfisf  21146  chfacfisfcpmat  21147  chcoeffeq  21178  cayhamlem3  21179  tx1stc  21942  ioorcl  23861  coemullem  24523  xrlimcnp  25228  fsumdvdscom  25444  fsumvma  25471  cusgrres  26913  usgredgsscusgredg  26924  clwlkclwwlklem2a  27463  clwwlkext2edg  27522  frgrwopreglem5ALT  27793  frgr2wwlkeu  27798  frgr2wwlk1  27800  grpoidinvlem3  27974  htthlem  28385  atcvat4i  29865  abfmpeld  30089  isarchi3  30454  ordtconnlem1  30784  gonarlem  32249  fmlasucdisj  32254  funpartfun  33013  relowlssretop  34175  ltflcei  34411  neificl  34560  keridl  34842  eqvrelth  35377  cvrat4  36110  ps-2  36145  mpaaeu  39235  clcnvlem  39468  iccpartiltu  43064  2pwp1prm  43233  bgoldbtbnd  43456  lmod0rng  43617  lincext1  43989