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 206  df-an 397

This theorem is referenced by:  sbc2iedv  3801  csbie2t  3873  frinxp  5669  ordelord  6288  foco2  6983  frxp  7967  mpocurryd  8085  omsmolem  8487  erth  8547  unblem1  9066  unwdomg  9343  cflim2  10019  distrlem1pr  10781  uz11  12607  elpq  12715  xmulge0  13018  max0add  15022  lcmfunsnlem2lem1  16343  divgcdcoprm0  16370  cncongr1  16372  prmpwdvds  16605  imasleval  17252  dfgrp3lem  18673  resscntz  18938  ablfac1c  19674  lbsind  20342  isphld  20859  mplcoe5lem  21240  cply1mul  21465  smadiadetr  21824  chfacfisf  22003  chfacfisfcpmat  22004  chcoeffeq  22035  cayhamlem3  22036  tx1stc  22801  ioorcl  24741  coemullem  25411  xrlimcnp  26118  fsumdvdscom  26334  fsumvma  26361  cusgrres  27815  usgredgsscusgredg  27826  clwlkclwwlklem2a  28362  clwwlkext2edg  28420  frgrwopreglem5ALT  28686  frgr2wwlkeu  28691  frgr2wwlk1  28693  grpoidinvlem3  28868  htthlem  29279  atcvat4i  30759  abfmpeld  30991  ressupprn  31024  isarchi3  31441  qsidomlem2  31629  ordtconnlem1  31874  gonarlem  33356  fmlasucdisj  33361  funpartfun  34245  relowlssretop  35534  ltflcei  35765  neificl  35911  keridl  36190  eqvrelth  36724  cvrat4  37457  ps-2  37492  mpaaeu  40975  clcnvlem  41231  fcoresf1  44563  iccpartiltu  44874  2pwp1prm  45041  bgoldbtbnd  45261  lmod0rng  45426  lincext1  45795