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  3827  csbie2t  3897  frinxp  5714  ordelord  6342  foco2  7063  f1ounsn  7229  frxp  8082  mpocurryd  8225  omsmolem  8598  erth  8702  unblem1  9215  unwdomg  9513  cflim2  10192  distrlem1pr  10954  uz11  12794  elpq  12910  xmulge0  13220  max0add  15252  lcmfunsnlem2lem1  16584  divgcdcoprm0  16611  cncongr1  16613  prmpwdvds  16851  imasleval  17480  issgrpd  18639  dfgrp3lem  18952  resscntz  19247  ablfac1c  19987  lbsind  21019  isphld  21596  mplcoe5lem  21979  cply1mul  22216  smadiadetr  22595  chfacfisf  22774  chfacfisfcpmat  22775  chcoeffeq  22806  cayhamlem3  22807  tx1stc  23570  ioorcl  25511  coemullem  26188  xrlimcnp  26911  fsumdvdscom  27128  fsumvma  27157  cusgrres  29429  usgredgsscusgredg  29440  clwlkclwwlklem2a  29977  clwwlkext2edg  30035  frgrwopreglem5ALT  30301  frgr2wwlkeu  30306  frgr2wwlk1  30308  grpoidinvlem3  30485  htthlem  30896  atcvat4i  32376  abfmpeld  32628  ressupprn  32663  isarchi3  33156  qsidomlem2  33417  ordtconnlem1  33907  gonarlem  35374  fmlasucdisj  35379  funpartfun  35924  relowlssretop  37344  ltflcei  37595  neificl  37740  keridl  38019  eqvrelth  38595  cvrat4  39430  ps-2  39465  mpaaeu  43132  clcnvlem  43605  fcoresf1  47063  modlt0b  47357  iccpartiltu  47416  2pwp1prm  47583  bgoldbtbnd  47803  isuspgrimlem  47888  grimedg  47928  grimgrtri  47941  lmod0rng  48210  lincext1  48436