Theorem impl 458

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sbc2iedv  3851  csbie2t  3921  frinxp  5634  ordelord  6213  foco2  6873  frxp  7820  mpocurryd  7935  omsmolem  8280  erth  8338  unblem1  8770  unwdomg  9048  cflim2  9685  distrlem1pr  10447  uz11  12268  elpq  12375  xmulge0  12678  max0add  14670  lcmfunsnlem2lem1  15982  divgcdcoprm0  16009  cncongr1  16011  prmpwdvds  16240  imasleval  16814  dfgrp3lem  18197  resscntz  18462  ablfac1c  19193  lbsind  19852  mplcoe5lem  20248  cply1mul  20462  isphld  20798  smadiadetr  21284  chfacfisf  21462  chfacfisfcpmat  21463  chcoeffeq  21494  cayhamlem3  21495  tx1stc  22258  ioorcl  24178  coemullem  24840  xrlimcnp  25546  fsumdvdscom  25762  fsumvma  25789  cusgrres  27230  usgredgsscusgredg  27241  clwlkclwwlklem2a  27776  clwwlkext2edg  27835  frgrwopreglem5ALT  28101  frgr2wwlkeu  28106  frgr2wwlk1  28108  grpoidinvlem3  28283  htthlem  28694  atcvat4i  30174  abfmpeld  30399  isarchi3  30816  qsidomlem2  30966  ordtconnlem1  31167  gonarlem  32641  fmlasucdisj  32646  funpartfun  33404  relowlssretop  34647  ltflcei  34895  neificl  35043  keridl  35325  eqvrelth  35861  cvrat4  36594  ps-2  36629  mpaaeu  39770  clcnvlem  40003  iccpartiltu  43602  2pwp1prm  43771  bgoldbtbnd  43994  lmod0rng  44159  lincext1  44529