Theorem impl 459

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sbc2iedv  3774  csbie2t  3843  frinxp  5603  ordelord  6191  foco2  6864  frxp  7825  mpocurryd  7945  omsmolem  8290  erth  8348  unblem1  8803  unwdomg  9081  cflim2  9723  distrlem1pr  10485  uz11  12307  elpq  12415  xmulge0  12718  max0add  14718  lcmfunsnlem2lem1  16034  divgcdcoprm0  16061  cncongr1  16063  prmpwdvds  16295  imasleval  16872  dfgrp3lem  18264  resscntz  18529  ablfac1c  19261  lbsind  19920  isphld  20419  mplcoe5lem  20799  cply1mul  21018  smadiadetr  21375  chfacfisf  21554  chfacfisfcpmat  21555  chcoeffeq  21586  cayhamlem3  21587  tx1stc  22350  ioorcl  24277  coemullem  24946  xrlimcnp  25653  fsumdvdscom  25869  fsumvma  25896  cusgrres  27337  usgredgsscusgredg  27348  clwlkclwwlklem2a  27882  clwwlkext2edg  27940  frgrwopreglem5ALT  28206  frgr2wwlkeu  28211  frgr2wwlk1  28213  grpoidinvlem3  28388  htthlem  28799  atcvat4i  30279  abfmpeld  30515  ressupprn  30548  isarchi3  30967  qsidomlem2  31150  ordtconnlem1  31395  gonarlem  32872  fmlasucdisj  32877  funpartfun  33794  relowlssretop  35060  ltflcei  35325  neificl  35471  keridl  35750  eqvrelth  36286  cvrat4  37019  ps-2  37054  mpaaeu  40467  clcnvlem  40696  iccpartiltu  44307  2pwp1prm  44474  bgoldbtbnd  44694  lmod0rng  44859  lincext1  45228