Theorem impel 506

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  equs5e  2457  elabgtOLD  3663  mob2  3711  ssn0rex  4355  reusv2lem2  5397  copsex2t  5492  reuop  6292  trssord  6381  trsuc  6451  funimass2  6631  fvelima  6957  fvmptf  7019  funfvima2  7232  funfvima3  7237  tfi  7841  suppssov1  8182  tposf2  8234  frrlem4  8273  wfrlem4OLD  8311  wfrlem10OLD  8317  ectocld  8777  mapsnd  8879  resixpfo  8929  f1oeng  8966  nneneq  9208  nneneqOLD  9220  nnsdomgOLD  9302  fiint  9323  fodomfi  9324  eqinf  9478  hartogslem1  9536  cantnf  9687  rankwflemb  9787  carden2a  9960  carduni  9975  harval2  9991  cardaleph  10083  alephval3  10104  dfac5  10122  cfcof  10268  axdc4lem  10449  nqereu  10923  recexsr  11101  seqcoll  14424  swrdswrd  14654  swrdccatin1  14674  swrdccatin2  14678  repswswrd  14733  climcau  15616  odd2np1  16283  lcmfunsnlem2lem2  16575  coprmproddvdslem  16598  dvdsprm  16639  vdwlem6  16918  imasvscafn  17482  dirref  18553  irredn1  20239  isdrngd  20389  isdrngdOLD  20391  psgnghm  21132  gsummoncoe1  21827  prdstopn  23131  cnextcn  23570  tnggrpr  24171  ovolctb  25006  dyadmbl  25116  itg1addlem4  25215  itg1addlem4OLD  25216  itg1le  25230  dvcnp2  25436  c1liplem1  25512  pserulm  25933  perfectlem2  26730  dchrisumlem2  26990  noresle  27197  bday1s  27329  axlowdimlem16  28212  wlkv0  28905  wlkp1lem1  28927  wlkswwlksf1o  29130  wspniunwspnon  29174  trlsegvdeglem1  29470  frcond4  29520  2clwwlk2clwwlk  29600  opabssi  31837  nn0xmulclb  31979  zarclsiin  32846  cusgr3cyclex  34122  satfun  34397  fundmpss  34733  gg-dvcnp2  35169  nn0prpw  35203  bj-restpw  35968  bj-prmoore  35991  domalom  36280  cover2  36578  disjlem18  37665  sticksstones11  40967  setindtr  41753  onov0suclim  42014  oe0suclim  42017  ofoaid1  42098  ofoaid2  42099  naddcnfcom  42106  naddcnfass  42109  climxlim2lem  44551  2reuimp  45813  fvelsetpreimafv  46045  imasetpreimafvbijlemfo  46063  reupr  46180  lighneallem4  46268  proththd  46272  lincresunit3  47152