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  2487  mob2  3673  ssn0rex  4306  reusv2lem2  5364  copsex2t  5469  reuop  6291  trssord  6374  trsuc  6447  funimass2  6616  fvelima  6943  fvmptf  7008  funfvima2  7230  funfvima3  7235  tfi  7849  suppssov1  8195  suppssov2  8196  tposf2  8248  frrlem4  8288  ectocld  8782  mapsnd  8893  resixpfo  8943  f1oeng  8976  nneneq  9200  fodomfi  9282  fiint  9296  eqinf  9455  hartogslem1  9514  cantnf  9672  rankwflemb  9775  carden2a  9971  carduni  9986  harval2  10002  cardaleph  10092  alephval3  10113  dfac5  10131  cfcof  10276  axdc4lem  10457  nqereu  10938  recexsr  11116  seqcoll  14529  swrdswrd  14774  swrdccatin1  14794  swrdccatin2  14798  repswswrd  14855  climcau  15758  odd2np1  16431  lcmfunsnlem2lem2  16729  coprmproddvdslem  16752  dvdsprm  16794  vdwlem6  17078  imasvscafn  17623  dirref  18689  irredn1  20567  isdrng5  20917  isdrngd  20931  isdrngdOLD  20933  psgnghm  21793  gsummoncoe1  22533  prdstopn  23854  cnextcn  24293  tnggrpr  24881  ovolctb  25718  dyadmbl  25828  itg1addlem4  25927  itg1le  25941  dvcnp2  26147  c1liplem1  26223  pserulm  26658  fsumdvdsmul  27431  perfectlem2  27466  dchrisumlem2  27726  noresle  27933  bday1  28079  readdscl  28764  remulscl  28767  axlowdimlem16  29414  wlkv0  30109  wlkp1lem1  30131  wlkswwlksf1o  30347  wspniunwspnon  30391  trlsegvdeglem1  30700  frcond4  30750  2clwwlk2clwwlk  30830  opabssi  33086  nn0xmulclb  33242  zarclsiin  34381  rankval4b  35607  cusgr3cyclex  35725  satfun  35990  fundmpss  36346  nn0prpw  36942  bj-restpw  37842  bj-prmoore  37865  cgsex2gd  37889  domalom  38158  cover2  38465  disjlem18  39651  sticksstones11  43022  setindtr  43865  onov0suclim  44115  oe0suclim  44118  ofoaid1  44199  ofoaid2  44200  naddcnfcom  44207  naddcnfass  44210  omssaxinf2  45811  climxlim2lem  46673  sge0f1o  47210  2reuimp  48003  fvelsetpreimafv  48287  imasetpreimafvbijlemfo  48305  reupr  48422  lighneallem4  48513  proththd  48517  lincresunit3  49411  oppc1stflem  50213