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  3832  csbie2t  3902  frinxp  5723  ordelord  6356  foco2  7083  f1ounsn  7249  frxp  8107  mpocurryd  8250  omsmolem  8623  erth  8727  unblem1  9245  unwdomg  9543  cflim2  10222  distrlem1pr  10984  uz11  12824  elpq  12940  xmulge0  13250  max0add  15282  lcmfunsnlem2lem1  16614  divgcdcoprm0  16641  cncongr1  16643  prmpwdvds  16881  imasleval  17510  issgrpd  18663  dfgrp3lem  18976  resscntz  19271  ablfac1c  20009  lbsind  20993  isphld  21569  mplcoe5lem  21952  cply1mul  22189  smadiadetr  22568  chfacfisf  22747  chfacfisfcpmat  22748  chcoeffeq  22779  cayhamlem3  22780  tx1stc  23543  ioorcl  25484  coemullem  26161  xrlimcnp  26884  fsumdvdscom  27101  fsumvma  27130  cusgrres  29382  usgredgsscusgredg  29393  clwlkclwwlklem2a  29933  clwwlkext2edg  29991  frgrwopreglem5ALT  30257  frgr2wwlkeu  30262  frgr2wwlk1  30264  grpoidinvlem3  30441  htthlem  30852  atcvat4i  32332  abfmpeld  32584  ressupprn  32619  isarchi3  33147  qsidomlem2  33430  ordtconnlem1  33920  gonarlem  35381  fmlasucdisj  35386  funpartfun  35926  relowlssretop  37346  ltflcei  37597  neificl  37742  keridl  38021  eqvrelth  38597  cvrat4  39432  ps-2  39467  mpaaeu  43132  clcnvlem  43605  fcoresf1  47060  modlt0b  47354  iccpartiltu  47413  2pwp1prm  47580  bgoldbtbnd  47800  isuspgrimlem  47885  grimedg  47925  grimgrtri  47938  lmod0rng  48207  lincext1  48433