Theorem impel 507

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  equs5e  2458  elabgtOLD  3664  mob2  3712  ssn0rex  4356  reusv2lem2  5398  copsex2t  5493  reuop  6293  trssord  6382  trsuc  6452  funimass2  6632  fvelima  6958  fvmptf  7020  funfvima2  7233  funfvima3  7238  tfi  7842  suppssov1  8183  tposf2  8235  frrlem4  8274  wfrlem4OLD  8312  wfrlem10OLD  8318  ectocld  8778  mapsnd  8880  resixpfo  8930  f1oeng  8967  nneneq  9209  nneneqOLD  9221  nnsdomgOLD  9303  fiint  9324  fodomfi  9325  eqinf  9479  hartogslem1  9537  cantnf  9688  rankwflemb  9788  carden2a  9961  carduni  9976  harval2  9992  cardaleph  10084  alephval3  10105  dfac5  10123  cfcof  10269  axdc4lem  10450  nqereu  10924  recexsr  11102  seqcoll  14425  swrdswrd  14655  swrdccatin1  14675  swrdccatin2  14679  repswswrd  14734  climcau  15617  odd2np1  16284  lcmfunsnlem2lem2  16576  coprmproddvdslem  16599  dvdsprm  16640  vdwlem6  16919  imasvscafn  17483  dirref  18554  irredn1  20240  isdrngd  20390  isdrngdOLD  20392  psgnghm  21133  gsummoncoe1  21828  prdstopn  23132  cnextcn  23571  tnggrpr  24172  ovolctb  25007  dyadmbl  25117  itg1addlem4  25216  itg1addlem4OLD  25217  itg1le  25231  dvcnp2  25437  c1liplem1  25513  pserulm  25934  perfectlem2  26733  dchrisumlem2  26993  noresle  27200  bday1s  27332  axlowdimlem16  28215  wlkv0  28908  wlkp1lem1  28930  wlkswwlksf1o  29133  wspniunwspnon  29177  trlsegvdeglem1  29473  frcond4  29523  2clwwlk2clwwlk  29603  opabssi  31842  nn0xmulclb  31984  zarclsiin  32851  cusgr3cyclex  34127  satfun  34402  fundmpss  34738  gg-dvcnp2  35174  nn0prpw  35208  bj-restpw  35973  bj-prmoore  35996  domalom  36285  cover2  36583  disjlem18  37670  sticksstones11  40972  setindtr  41763  onov0suclim  42024  oe0suclim  42027  ofoaid1  42108  ofoaid2  42109  naddcnfcom  42116  naddcnfass  42119  climxlim2lem  44561  2reuimp  45823  fvelsetpreimafv  46055  imasetpreimafvbijlemfo  46073  reupr  46190  lighneallem4  46278  proththd  46282  lincresunit3  47162