Theorem impl 461

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbc2iedv  3822  csbie2t  3892  frinxp  5746  ordelord  6386  foco2  7108  f1ounsn  7279  frxp  8128  mpocurryd  8271  omsmolem  8649  erth  8755  unblem1  9259  unwdomg  9553  cflim2  10262  distrlem1pr  11029  uz11  12907  elpq  13019  xmulge0  13330  max0add  15389  lcmfunsnlem2lem1  16722  divgcdcoprm0  16749  cncongr1  16751  prmpwdvds  16990  imasleval  17621  issgrpd  18824  dfgrp3lem  19152  resscntz  19451  ablfac1c  20191  lbsind  21255  qsidomlem2  21535  isphld  21858  mplcoe5lem  22244  cply1mul  22510  smadiadetr  22886  chfacfisf  23065  chfacfisfcpmat  23066  chcoeffeq  23097  cayhamlem3  23098  tx1stc  23862  ioorcl  25791  coemullem  26462  xrlimcnp  27188  fsumdvdscom  27404  fsumvma  27432  cusgrres  29860  usgredgsscusgredg  29871  clwlkclwwlklem2a  30420  clwwlkext2edg  30478  frgrwopreglem5ALT  30748  frgr2wwlkeu  30753  frgr2wwlk1  30755  grpoidinvlem3  30933  htthlem  31344  atcvat4i  32824  abfmpeld  33074  ressupprn  33110  isarchi3  33575  ordtconnlem1  34382  gonarlem  35927  fmlasucdisj  35932  funpartfun  36476  relowlssretop  38070  ltflcei  38320  neificl  38466  keridl  38745  eqvrelth  39406  cvrat4  40279  ps-2  40314  mpaaeu  43954  clcnvlem  44426  fcoresf1  47883  modlt0b  48183  iccpartiltu  48248  2pwp1prm  48418  bgoldbtbnd  48651  isuspgrimlem  48737  grimedg  48777  grimgrtri  48791  lmod0rng  49070  lincext1  49310