Theorem impl 454

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 414	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 416	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sbc2iedv  3859  csbie2t  3931  frinxp  5759  ordelord  6391  foco2  7116  frxp  8129  mpocurryd  8273  omsmolem  8676  erth  8773  unblem1  9318  unwdomg  9607  cflim2  10286  distrlem1pr  11048  uz11  12877  elpq  12989  xmulge0  13295  max0add  15289  lcmfunsnlem2lem1  16608  divgcdcoprm0  16635  cncongr1  16637  prmpwdvds  16872  imasleval  17522  issgrpd  18689  dfgrp3lem  18998  resscntz  19288  ablfac1c  20032  lbsind  20969  isphld  21590  mplcoe5lem  21984  cply1mul  22224  smadiadetr  22607  chfacfisf  22786  chfacfisfcpmat  22787  chcoeffeq  22818  cayhamlem3  22819  tx1stc  23584  ioorcl  25536  coemullem  26214  xrlimcnp  26930  fsumdvdscom  27147  fsumvma  27176  cusgrres  29318  usgredgsscusgredg  29329  clwlkclwwlklem2a  29864  clwwlkext2edg  29922  frgrwopreglem5ALT  30188  frgr2wwlkeu  30193  frgr2wwlk1  30195  grpoidinvlem3  30372  htthlem  30783  atcvat4i  32263  abfmpeld  32497  ressupprn  32527  isarchi3  32952  qsidomlem2  33231  ordtconnlem1  33595  gonarlem  35074  fmlasucdisj  35079  funpartfun  35609  relowlssretop  36912  ltflcei  37151  neificl  37296  keridl  37575  eqvrelth  38152  cvrat4  38985  ps-2  39020  mpaaeu  42639  clcnvlem  43118  fcoresf1  46514  iccpartiltu  46825  2pwp1prm  46992  bgoldbtbnd  47212  isuspgrimlem  47284  lmod0rng  47403  lincext1  47634