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  3847  csbie2t  3917  frinxp  5742  ordelord  6379  foco2  7104  f1ounsn  7270  frxp  8130  mpocurryd  8273  omsmolem  8674  erth  8775  unblem1  9305  unwdomg  9603  cflim2  10282  distrlem1pr  11044  uz11  12882  elpq  12996  xmulge0  13305  max0add  15334  lcmfunsnlem2lem1  16662  divgcdcoprm0  16689  cncongr1  16691  prmpwdvds  16929  imasleval  17560  issgrpd  18713  dfgrp3lem  19026  resscntz  19321  ablfac1c  20059  lbsind  21043  isphld  21619  mplcoe5lem  22002  cply1mul  22239  smadiadetr  22618  chfacfisf  22797  chfacfisfcpmat  22798  chcoeffeq  22829  cayhamlem3  22830  tx1stc  23593  ioorcl  25535  coemullem  26212  xrlimcnp  26935  fsumdvdscom  27152  fsumvma  27181  cusgrres  29433  usgredgsscusgredg  29444  clwlkclwwlklem2a  29984  clwwlkext2edg  30042  frgrwopreglem5ALT  30308  frgr2wwlkeu  30313  frgr2wwlk1  30315  grpoidinvlem3  30492  htthlem  30903  atcvat4i  32383  abfmpeld  32637  ressupprn  32672  isarchi3  33190  qsidomlem2  33473  ordtconnlem1  33960  gonarlem  35421  fmlasucdisj  35426  funpartfun  35966  relowlssretop  37386  ltflcei  37637  neificl  37782  keridl  38061  eqvrelth  38634  cvrat4  39467  ps-2  39502  mpaaeu  43149  clcnvlem  43622  fcoresf1  47078  iccpartiltu  47416  2pwp1prm  47583  bgoldbtbnd  47803  isuspgrimlem  47888  grimedg  47928  grimgrtri  47941  lmod0rng  48184  lincext1  48410