Theorem impel 509

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

Ref	Expression
impel.1	⊢ (𝜑 → (𝜓 → 𝜒))
impel.2	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
impel	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 410	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:  equs5e  2470  elabgt  3609  mob2  3654  ssn0rex  4269  csb0  4314  reusv2lem2  5265  copsex2t  5348  reuop  6112  trssord  6176  trsuc  6243  funimass2  6407  fvelima  6706  fvmptf  6766  funfvima2  6971  funfvima3  6976  tfi  7548  suppssov1  7845  tposf2  7899  wfrlem4  7941  wfrlem10  7947  ectocld  8347  mapsnd  8433  resixpfo  8483  f1oeng  8511  nneneq  8684  nnsdomg  8761  fiint  8779  fodomfi  8781  eqinf  8932  hartogslem1  8990  cantnf  9140  rankwflemb  9206  carden2a  9379  carduni  9394  harval2  9410  cardaleph  9500  alephval3  9521  dfac5  9539  cfcof  9685  axdc4lem  9866  nqereu  10340  recexsr  10518  seqcoll  13818  swrdswrd  14058  swrdccatin1  14078  swrdccatin2  14082  repswswrd  14137  climcau  15019  odd2np1  15682  lcmfunsnlem2lem2  15973  coprmproddvdslem  15996  dvdsprm  16037  vdwlem6  16312  imasvscafn  16802  dirref  17837  irredn1  19452  isdrngd  19520  psgnghm  20269  gsummoncoe1  20933  prdstopn  22233  cnextcn  22672  tnggrpr  23261  ovolctb  24094  dyadmbl  24204  itg1addlem4  24303  itg1le  24317  dvcnp2  24523  c1liplem1  24599  pserulm  25017  perfectlem2  25814  dchrisumlem2  26074  axlowdimlem16  26751  wlkv0  27440  wlkp1lem1  27463  wlkswwlksf1o  27665  wspniunwspnon  27709  trlsegvdeglem1  28005  frcond4  28055  2clwwlk2clwwlk  28135  opabssi  30377  nn0xmulclb  30522  zarclsiin  31224  cusgr3cyclex  32496  satfun  32771  fundmpss  33122  frrlem4  33239  noresle  33313  nn0prpw  33784  bj-restpw  34507  bj-prmoore  34530  domalom  34821  cover2  35152  setindtr  39965  climxlim2lem  42487  2reuimp  43671  fvelsetpreimafv  43904  imasetpreimafvbijlemfo  43922  reupr  44039  lighneallem4  44128  proththd  44132  lincresunit3  44890