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  3806  csbie2t  3876  frinxp  5709  ordelord  6341  foco2  7057  f1ounsn  7222  frxp  8071  mpocurryd  8214  omsmolem  8588  erth  8693  unblem1  9197  unwdomg  9494  cflim2  10180  distrlem1pr  10943  uz11  12808  elpq  12920  xmulge0  13231  max0add  15267  lcmfunsnlem2lem1  16602  divgcdcoprm0  16629  cncongr1  16631  prmpwdvds  16870  imasleval  17500  issgrpd  18693  dfgrp3lem  19009  resscntz  19303  ablfac1c  20043  lbsind  21071  isphld  21648  mplcoe5lem  22031  cply1mul  22275  smadiadetr  22654  chfacfisf  22833  chfacfisfcpmat  22834  chcoeffeq  22865  cayhamlem3  22866  tx1stc  23629  ioorcl  25558  coemullem  26229  xrlimcnp  26949  fsumdvdscom  27166  fsumvma  27194  cusgrres  29536  usgredgsscusgredg  29547  clwlkclwwlklem2a  30087  clwwlkext2edg  30145  frgrwopreglem5ALT  30411  frgr2wwlkeu  30416  frgr2wwlk1  30418  grpoidinvlem3  30596  htthlem  31007  atcvat4i  32487  abfmpeld  32746  ressupprn  32782  isarchi3  33267  qsidomlem2  33532  ordtconnlem1  34088  gonarlem  35596  fmlasucdisj  35601  funpartfun  36145  relowlssretop  37697  ltflcei  37947  neificl  38092  keridl  38371  eqvrelth  39034  cvrat4  39907  ps-2  39942  mpaaeu  43600  clcnvlem  44072  fcoresf1  47533  modlt0b  47833  iccpartiltu  47898  2pwp1prm  48068  bgoldbtbnd  48301  isuspgrimlem  48387  grimedg  48427  grimgrtri  48441  lmod0rng  48721  lincext1  48946