Theorem impel 515

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  equs5e  2492  mob2  3680  ssn0rex  4313  reusv2lem2  5372  copsex2t  5477  reuop  6298  trssord  6381  trsuc  6454  funimass2  6623  fvelima  6950  fvmptf  7015  funfvima2  7233  funfvima3  7238  tfi  7851  suppssov1  8195  suppssov2  8196  tposf2  8248  frrlem4  8288  ectocld  8782  mapsnd  8886  resixpfo  8936  f1oeng  8969  nneneq  9193  fodomfi  9275  fiint  9289  eqinf  9448  hartogslem1  9507  cantnf  9665  rankwflemb  9768  carden2a  9964  carduni  9979  harval2  9995  cardaleph  10085  alephval3  10106  dfac5  10124  cfcof  10269  axdc4lem  10450  nqereu  10925  recexsr  11103  seqcoll  14515  swrdswrd  14760  swrdccatin1  14780  swrdccatin2  14784  repswswrd  14841  climcau  15742  odd2np1  16417  lcmfunsnlem2lem2  16715  coprmproddvdslem  16738  dvdsprm  16780  vdwlem6  17064  imasvscafn  17609  dirref  18675  irredn1  20534  isdrng5  20884  isdrngd  20898  isdrngdOLD  20900  psgnghm  21760  gsummoncoe1  22498  prdstopn  23816  cnextcn  24255  tnggrpr  24843  ovolctb  25680  dyadmbl  25790  itg1addlem4  25889  itg1le  25903  dvcnp2  26110  c1liplem1  26186  pserulm  26616  fsumdvdsmul  27390  perfectlem2  27425  dchrisumlem2  27685  noresle  27892  bday1  28038  readdscl  28723  remulscl  28726  axlowdimlem16  29338  wlkv0  30033  wlkp1lem1  30055  wlkswwlksf1o  30271  wspniunwspnon  30315  trlsegvdeglem1  30618  frcond4  30668  2clwwlk2clwwlk  30748  opabssi  33005  nn0xmulclb  33162  zarclsiin  34301  rankval4b  35527  cusgr3cyclex  35645  satfun  35916  fundmpss  36272  nn0prpw  36867  bj-restpw  37767  bj-prmoore  37790  cgsex2gd  37814  domalom  38083  cover2  38399  disjlem18  39585  sticksstones11  42956  setindtr  43784  onov0suclim  44034  oe0suclim  44037  ofoaid1  44118  ofoaid2  44119  naddcnfcom  44126  naddcnfass  44129  omssaxinf2  45730  climxlim2lem  46592  sge0f1o  47129  2reuimp  47885  fvelsetpreimafv  48169  imasetpreimafvbijlemfo  48187  reupr  48304  lighneallem4  48395  proththd  48399  lincresunit3  49294  oppc1stflem  50098