Theorem impl 455

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

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  sbc2iedv  3883  csbie2t  3956  frinxp  5781  ordelord  6416  foco2  7141  frxp  8163  mpocurryd  8306  omsmolem  8709  erth  8810  unblem1  9352  unwdomg  9649  cflim2  10328  distrlem1pr  11090  uz11  12924  elpq  13036  xmulge0  13342  max0add  15355  lcmfunsnlem2lem1  16679  divgcdcoprm0  16706  cncongr1  16708  prmpwdvds  16946  imasleval  17596  issgrpd  18763  dfgrp3lem  19073  resscntz  19368  ablfac1c  20110  lbsind  21097  isphld  21690  mplcoe5lem  22074  cply1mul  22314  smadiadetr  22695  chfacfisf  22874  chfacfisfcpmat  22875  chcoeffeq  22906  cayhamlem3  22907  tx1stc  23672  ioorcl  25624  coemullem  26301  xrlimcnp  27020  fsumdvdscom  27237  fsumvma  27266  cusgrres  29475  usgredgsscusgredg  29486  clwlkclwwlklem2a  30021  clwwlkext2edg  30079  frgrwopreglem5ALT  30345  frgr2wwlkeu  30350  frgr2wwlk1  30352  grpoidinvlem3  30529  htthlem  30940  atcvat4i  32420  abfmpeld  32664  ressupprn  32694  isarchi3  33159  qsidomlem2  33438  ordtconnlem1  33862  gonarlem  35354  fmlasucdisj  35359  funpartfun  35899  relowlssretop  37277  ltflcei  37516  neificl  37661  keridl  37940  eqvrelth  38515  cvrat4  39348  ps-2  39383  mpaaeu  43047  clcnvlem  43525  fcoresf1  46918  iccpartiltu  47228  2pwp1prm  47395  bgoldbtbnd  47615  isuspgrimlem  47687  grimedg  47716  grimgrtri  47726  lmod0rng  47870  lincext1  48101