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  3889  csbie2t  3962  frinxp  5782  ordelord  6417  foco2  7143  frxp  8167  mpocurryd  8310  omsmolem  8713  erth  8814  unblem1  9356  unwdomg  9653  cflim2  10332  distrlem1pr  11094  uz11  12928  elpq  13040  xmulge0  13346  max0add  15359  lcmfunsnlem2lem1  16685  divgcdcoprm0  16712  cncongr1  16714  prmpwdvds  16951  imasleval  17601  issgrpd  18768  dfgrp3lem  19078  resscntz  19373  ablfac1c  20115  lbsind  21102  isphld  21695  mplcoe5lem  22080  cply1mul  22321  smadiadetr  22702  chfacfisf  22881  chfacfisfcpmat  22882  chcoeffeq  22913  cayhamlem3  22914  tx1stc  23679  ioorcl  25631  coemullem  26309  xrlimcnp  27029  fsumdvdscom  27246  fsumvma  27275  cusgrres  29484  usgredgsscusgredg  29495  clwlkclwwlklem2a  30030  clwwlkext2edg  30088  frgrwopreglem5ALT  30354  frgr2wwlkeu  30359  frgr2wwlk1  30361  grpoidinvlem3  30538  htthlem  30949  atcvat4i  32429  abfmpeld  32672  ressupprn  32702  isarchi3  33167  qsidomlem2  33446  ordtconnlem1  33870  gonarlem  35362  fmlasucdisj  35367  funpartfun  35907  relowlssretop  37329  ltflcei  37568  neificl  37713  keridl  37992  eqvrelth  38567  cvrat4  39400  ps-2  39435  mpaaeu  43107  clcnvlem  43585  fcoresf1  46984  iccpartiltu  47296  2pwp1prm  47463  bgoldbtbnd  47683  isuspgrimlem  47758  grimedg  47787  grimgrtri  47798  lmod0rng  47952  lincext1  48183