Theorem impel 514

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 35	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 411	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  equs5e  2496  mob2  3687  ssn0rex  4320  reusv2lem2  5368  copsex2t  5473  reuop  6291  trssord  6374  trsuc  6447  funimass2  6616  fvelima  6944  fvmptf  7009  funfvima2  7227  funfvima3  7232  tfi  7845  suppssov1  8189  suppssov2  8190  tposf2  8242  frrlem4  8282  ectocld  8776  mapsnd  8880  resixpfo  8930  f1oeng  8963  nneneq  9186  fodomfi  9268  fiint  9282  eqinf  9441  hartogslem1  9500  cantnf  9658  rankwflemb  9761  carden2a  9948  carduni  9963  harval2  9979  cardaleph  10069  alephval3  10090  dfac5  10108  cfcof  10254  axdc4lem  10435  nqereu  10910  recexsr  11088  seqcoll  14497  swrdswrd  14738  swrdccatin1  14758  swrdccatin2  14762  repswswrd  14817  climcau  15718  odd2np1  16395  lcmfunsnlem2lem2  16693  coprmproddvdslem  16716  dvdsprm  16758  vdwlem6  17042  imasvscafn  17587  dirref  18653  irredn1  20504  isdrngd  20843  isdrngdOLD  20845  psgnghm  21695  gsummoncoe1  22433  prdstopn  23750  cnextcn  24189  tnggrpr  24777  ovolctb  25614  dyadmbl  25724  itg1addlem4  25823  itg1le  25837  dvcnp2  26044  c1liplem1  26120  pserulm  26547  fsumdvdsmul  27321  perfectlem2  27356  dchrisumlem2  27616  noresle  27823  bday1  27969  readdscl  28654  remulscl  28657  axlowdimlem16  29244  wlkv0  29936  wlkp1lem1  29958  wlkswwlksf1o  30165  wspniunwspnon  30209  trlsegvdeglem1  30508  frcond4  30558  2clwwlk2clwwlk  30638  opabssi  32895  nn0xmulclb  33053  zarclsiin  34202  rankval4b  35432  cusgr3cyclex  35523  satfun  35798  fundmpss  36154  nn0prpw  36719  bj-restpw  37617  bj-prmoore  37640  cgsex2gd  37664  domalom  37933  cover2  38249  disjlem18  39437  sticksstones11  42808  setindtr  43636  onov0suclim  43886  oe0suclim  43889  ofoaid1  43970  ofoaid2  43971  naddcnfcom  43978  naddcnfass  43981  omssaxinf2  45582  climxlim2lem  46444  sge0f1o  46981  2reuimp  47734  fvelsetpreimafv  48018  imasetpreimafvbijlemfo  48036  reupr  48153  lighneallem4  48244  proththd  48248  lincresunit3  49139  oppc1stflem  49943