Theorem impel 505

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  equs5e  2456  mob2  3683  ssn0rex  4317  reusv2lem2  5349  copsex2t  5447  reuop  6254  trssord  6337  trsuc  6409  funimass2  6583  fvelima  6908  fvmptf  6971  funfvima2  7187  funfvima3  7192  tfi  7809  suppssov1  8153  suppssov2  8154  tposf2  8206  frrlem4  8245  ectocld  8732  mapsnd  8836  resixpfo  8886  f1oeng  8919  nneneq  9147  nnsdomgOLD  9223  fodomfi  9237  fiint  9253  fiintOLD  9254  fodomfiOLD  9257  eqinf  9412  hartogslem1  9471  cantnf  9622  rankwflemb  9722  carden2a  9895  carduni  9910  harval2  9926  cardaleph  10018  alephval3  10039  dfac5  10058  cfcof  10203  axdc4lem  10384  nqereu  10858  recexsr  11036  seqcoll  14405  swrdswrd  14646  swrdccatin1  14666  swrdccatin2  14670  repswswrd  14725  climcau  15613  odd2np1  16287  lcmfunsnlem2lem2  16585  coprmproddvdslem  16608  dvdsprm  16649  vdwlem6  16933  imasvscafn  17476  dirref  18536  irredn1  20311  isdrngd  20650  isdrngdOLD  20652  psgnghm  21465  gsummoncoe1  22171  prdstopn  23491  cnextcn  23930  tnggrpr  24519  ovolctb  25367  dyadmbl  25477  itg1addlem4  25576  itg1le  25590  dvcnp2  25797  dvcnp2OLD  25798  c1liplem1  25877  pserulm  26307  fsumdvdsmul  27081  perfectlem2  27117  dchrisumlem2  27377  noresle  27585  bday1s  27719  readdscl  28326  remulscl  28329  axlowdimlem16  28860  wlkv0  29553  wlkp1lem1  29575  wlkswwlksf1o  29782  wspniunwspnon  29826  trlsegvdeglem1  30122  frcond4  30172  2clwwlk2clwwlk  30252  opabssi  32514  nn0xmulclb  32667  zarclsiin  33834  cusgr3cyclex  35096  satfun  35371  fundmpss  35727  nn0prpw  36284  bj-restpw  37053  bj-prmoore  37076  domalom  37365  cover2  37682  disjlem18  38765  sticksstones11  42117  setindtr  42986  onov0suclim  43236  oe0suclim  43239  ofoaid1  43320  ofoaid2  43321  naddcnfcom  43328  naddcnfass  43331  omssaxinf2  44951  climxlim2lem  45816  sge0f1o  46353  2reuimp  47089  fvelsetpreimafv  47361  imasetpreimafvbijlemfo  47379  reupr  47496  lighneallem4  47584  proththd  47588  lincresunit3  48443  oppc1stflem  49249