Theorem impel 504

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 405	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  equs5e  2451  elabgtOLDOLD  3659  mob2  3707  ssn0rex  4355  reusv2lem2  5399  copsex2t  5494  reuop  6299  trssord  6388  trsuc  6458  funimass2  6637  fvelima  6963  fvmptf  7025  funfvima2  7243  funfvima3  7248  tfi  7858  suppssov1  8203  suppssov2  8204  tposf2  8256  frrlem4  8295  wfrlem4OLD  8333  wfrlem10OLD  8339  ectocld  8803  mapsnd  8905  resixpfo  8955  f1oeng  8992  nneneq  9234  nneneqOLD  9246  nnsdomgOLD  9328  fiint  9350  fodomfi  9351  eqinf  9509  hartogslem1  9567  cantnf  9718  rankwflemb  9818  carden2a  9991  carduni  10006  harval2  10022  cardaleph  10114  alephval3  10135  dfac5  10153  cfcof  10299  axdc4lem  10480  nqereu  10954  recexsr  11132  seqcoll  14461  swrdswrd  14691  swrdccatin1  14711  swrdccatin2  14715  repswswrd  14770  climcau  15653  odd2np1  16321  lcmfunsnlem2lem2  16613  coprmproddvdslem  16636  dvdsprm  16677  vdwlem6  16958  imasvscafn  17522  dirref  18596  irredn1  20377  isdrngd  20669  isdrngdOLD  20671  psgnghm  21529  gsummoncoe1  22252  prdstopn  23576  cnextcn  24015  tnggrpr  24616  ovolctb  25463  dyadmbl  25573  itg1addlem4  25672  itg1addlem4OLD  25673  itg1le  25687  dvcnp2  25893  dvcnp2OLD  25894  c1liplem1  25973  pserulm  26403  fsumdvdsmul  27172  perfectlem2  27208  dchrisumlem2  27468  noresle  27676  bday1s  27810  readdscl  28299  remulscl  28302  axlowdimlem16  28840  wlkv0  29537  wlkp1lem1  29559  wlkswwlksf1o  29762  wspniunwspnon  29806  trlsegvdeglem1  30102  frcond4  30152  2clwwlk2clwwlk  30232  opabssi  32482  nn0xmulclb  32623  zarclsiin  33603  cusgr3cyclex  34877  satfun  35152  fundmpss  35493  nn0prpw  35938  bj-restpw  36702  bj-prmoore  36725  domalom  37014  cover2  37319  disjlem18  38402  sticksstones11  41759  setindtr  42587  onov0suclim  42845  oe0suclim  42848  ofoaid1  42929  ofoaid2  42930  naddcnfcom  42937  naddcnfass  42940  climxlim2lem  45371  2reuimp  46633  fvelsetpreimafv  46864  imasetpreimafvbijlemfo  46882  reupr  46999  lighneallem4  47087  proththd  47091  lincresunit3  47735