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  3816  csbie2t  3886  frinxp  5697  ordelord  6324  foco2  7037  f1ounsn  7201  frxp  8051  mpocurryd  8194  omsmolem  8567  erth  8671  unblem1  9171  unwdomg  9465  cflim2  10146  distrlem1pr  10908  uz11  12749  elpq  12865  xmulge0  13175  max0add  15209  lcmfunsnlem2lem1  16541  divgcdcoprm0  16568  cncongr1  16570  prmpwdvds  16808  imasleval  17437  issgrpd  18630  dfgrp3lem  18943  resscntz  19238  ablfac1c  19978  lbsind  21007  isphld  21584  mplcoe5lem  21967  cply1mul  22204  smadiadetr  22583  chfacfisf  22762  chfacfisfcpmat  22763  chcoeffeq  22794  cayhamlem3  22795  tx1stc  23558  ioorcl  25498  coemullem  26175  xrlimcnp  26898  fsumdvdscom  27115  fsumvma  27144  cusgrres  29420  usgredgsscusgredg  29431  clwlkclwwlklem2a  29968  clwwlkext2edg  30026  frgrwopreglem5ALT  30292  frgr2wwlkeu  30297  frgr2wwlk1  30299  grpoidinvlem3  30476  htthlem  30887  atcvat4i  32367  abfmpeld  32626  ressupprn  32661  isarchi3  33146  qsidomlem2  33408  ordtconnlem1  33927  gonarlem  35406  fmlasucdisj  35411  funpartfun  35956  relowlssretop  37376  ltflcei  37627  neificl  37772  keridl  38051  eqvrelth  38627  cvrat4  39461  ps-2  39496  mpaaeu  43162  clcnvlem  43635  fcoresf1  47079  modlt0b  47373  iccpartiltu  47432  2pwp1prm  47599  bgoldbtbnd  47819  isuspgrimlem  47905  grimedg  47945  grimgrtri  47959  lmod0rng  48239  lincext1  48465