Theorem impl 457

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  sbc2iedv  3863  csbie2t  3935  frinxp  5759  ordelord  6387  foco2  7109  frxp  8112  mpocurryd  8254  omsmolem  8656  erth  8752  unblem1  9295  unwdomg  9579  cflim2  10258  distrlem1pr  11020  uz11  12847  elpq  12959  xmulge0  13263  max0add  15257  lcmfunsnlem2lem1  16575  divgcdcoprm0  16602  cncongr1  16604  prmpwdvds  16837  imasleval  17487  issgrpd  18621  dfgrp3lem  18921  resscntz  19197  ablfac1c  19941  lbsind  20691  isphld  21207  mplcoe5lem  21594  cply1mul  21818  smadiadetr  22177  chfacfisf  22356  chfacfisfcpmat  22357  chcoeffeq  22388  cayhamlem3  22389  tx1stc  23154  ioorcl  25094  coemullem  25764  xrlimcnp  26473  fsumdvdscom  26689  fsumvma  26716  cusgrres  28705  usgredgsscusgredg  28716  clwlkclwwlklem2a  29251  clwwlkext2edg  29309  frgrwopreglem5ALT  29575  frgr2wwlkeu  29580  frgr2wwlk1  29582  grpoidinvlem3  29759  htthlem  30170  atcvat4i  31650  abfmpeld  31879  ressupprn  31912  isarchi3  32333  qsidomlem2  32572  ordtconnlem1  32904  gonarlem  34385  fmlasucdisj  34390  funpartfun  34915  relowlssretop  36244  ltflcei  36476  neificl  36621  keridl  36900  eqvrelth  37481  cvrat4  38314  ps-2  38349  mpaaeu  41892  clcnvlem  42374  fcoresf1  45779  iccpartiltu  46090  2pwp1prm  46257  bgoldbtbnd  46477  lmod0rng  46642  lincext1  47135