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  2490  mob2  3676  ssn0rex  4309  reusv2lem2  5368  copsex2t  5471  reuop  6322  trssord  6405  trsuc  6478  funimass2  6653  fvelima  6981  fvmptf  7046  funfvima2  7268  funfvima3  7273  tfi  7898  suppssov1  8252  suppssov2  8253  tposf2  8305  frrlem4  8345  ectocld  8841  mapsnd  8952  resixpfo  9002  f1oeng  9035  nneneq  9259  fodomfi  9342  fiint  9356  eqinf  9514  hartogslem1  9573  cantnf  9731  rankwflemb  9837  rankwflembOLD  9838  rankval4b  9917  carden2a  10084  carduni  10101  harval2  10117  cardaleph  10207  alephval3  10228  dfac5  10246  cfcof  10391  axdc4lem  10572  nqereu  11053  recexsr  11231  seqcoll  14650  swrdswrd  14896  swrdccatin1  14916  swrdccatin2  14920  repswswrd  14977  climcau  15882  odd2np1  16555  lcmfunsnlem2lem2  16858  coprmproddvdslem  16881  dvdsprm  16923  vdwlem6  17208  imasvscafn  17759  dirref  18825  irredn1  20707  isdrng5  21059  isdrngd  21073  isdrngdOLD  21075  psgnghm  21941  gsummoncoe1  22681  prdstopn  24002  cnextcn  24441  tnggrpr  25029  ovolctb  25866  dyadmbl  25976  itg1addlem4  26075  itg1le  26089  dvcnp2  26295  c1liplem1  26371  pserulm  26806  fsumdvdsmul  27579  perfectlem2  27614  dchrisumlem2  27874  noresle  28111  bday1  28257  readdscl  28942  remulscl  28945  axlowdimlem16  29592  wlkv0  30287  wlkp1lem1  30309  wlkswwlksf1o  30525  wspniunwspnon  30569  trlsegvdeglem1  30878  frcond4  30928  2clwwlk2clwwlk  31008  opabssi  33305  nn0xmulclb  33459  zarclsiin  34614  cusgr3cyclex  36109  satfun  36384  elpssmo  36673  fundmpss  36747  nn0prpw  37326  bj-restpw  38283  bj-prmoore  38306  cgsex2gd  38329  domalom  38595  cover2  38917  disjlem18  40101  sticksstones11  43472  setindtr  44297  onov0suclim  44537  oe0suclim  44540  ofoaid1  44621  ofoaid2  44622  naddcnfcom  44629  naddcnfass  44632  omssaxinf2  46242  climxlim2lem  47128  sge0f1o  47665  2reuimp  48459  fvelsetpreimafv  48742  imasetpreimafvbijlemfo  48760  reupr  48877  lighneallem4  48968  proththd  48972  lincresunit3  49924  oppc1stflem  50740