Theorem impel 501

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  equs5e  2424  elabgt  3553  mob2  3598  ssn0rex  4164  reusv2lem2  5113  copsex2t  5190  trssord  5995  trsuc  6062  funimass2  6219  fvelima  6510  fvmptf  6564  funfvima2  6767  funfvima3  6770  tfi  7333  suppssov1  7611  tposf2  7660  wfrlem4  7702  wfrlem10  7709  ectocld  8099  mapsnd  8185  resixpfo  8234  f1oeng  8262  nneneq  8433  nnsdomg  8509  fiint  8527  fodomfi  8529  eqinf  8680  hartogslem1  8738  cantnf  8889  rankwflemb  8955  carden2a  9127  carduni  9142  harval2  9158  cardaleph  9247  alephval3  9268  dfac5  9286  cfcof  9433  axdc4lem  9614  nqereu  10088  recexsr  10266  seqcoll  13568  swrdswrd  13820  swrdccatin2  13862  repswswrd  13936  climcau  14818  odd2np1  15479  lcmfunsnlem2lem2  15768  coprmproddvdslem  15791  dvdsprm  15830  vdwlem6  16105  imasvscafn  16594  dirref  17632  irredn1  19104  isdrngd  19175  gsummoncoe1  20081  psgnghm  20332  prdstopn  21851  cnextcn  22290  tnggrpr  22878  ovolctb  23705  dyadmbl  23815  itg1addlem4  23914  itg1le  23928  wlkv0  27015  wlkp1lem1  27041  wlkswwlksf1o  27245  wspniunwspnon  27320  trlsegvdeglem1  27641  frcond4  27695  2clwwlk2clwwlk  27778  2clwwlk2clwwlkOLD  27779  opabssi  30005  frrlem4  32380  noresle  32443  bj-restpw  33626  cnfinltrel  33843  cover2  34142  setindtr  38564  climxlim2lem  40999  2reuimp  42170  lighneallem4  42562  proththd  42566  lincresunit3  43299