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  3686  ssn0rex  4321  reusv2lem2  5354  copsex2t  5452  reuop  6266  trssord  6349  trsuc  6421  funimass2  6599  fvelima  6926  fvmptf  6989  funfvima2  7205  funfvima3  7210  tfi  7829  suppssov1  8176  suppssov2  8177  tposf2  8229  frrlem4  8268  ectocld  8755  mapsnd  8859  resixpfo  8909  f1oeng  8942  nneneq  9170  nnsdomgOLD  9247  fodomfi  9261  fiint  9277  fiintOLD  9278  fodomfiOLD  9281  eqinf  9436  hartogslem1  9495  cantnf  9646  rankwflemb  9746  carden2a  9919  carduni  9934  harval2  9950  cardaleph  10042  alephval3  10063  dfac5  10082  cfcof  10227  axdc4lem  10408  nqereu  10882  recexsr  11060  seqcoll  14429  swrdswrd  14670  swrdccatin1  14690  swrdccatin2  14694  repswswrd  14749  climcau  15637  odd2np1  16311  lcmfunsnlem2lem2  16609  coprmproddvdslem  16632  dvdsprm  16673  vdwlem6  16957  imasvscafn  17500  dirref  18560  irredn1  20335  isdrngd  20674  isdrngdOLD  20676  psgnghm  21489  gsummoncoe1  22195  prdstopn  23515  cnextcn  23954  tnggrpr  24543  ovolctb  25391  dyadmbl  25501  itg1addlem4  25600  itg1le  25614  dvcnp2  25821  dvcnp2OLD  25822  c1liplem1  25901  pserulm  26331  fsumdvdsmul  27105  perfectlem2  27141  dchrisumlem2  27401  noresle  27609  bday1s  27743  readdscl  28350  remulscl  28353  axlowdimlem16  28884  wlkv0  29579  wlkp1lem1  29601  wlkswwlksf1o  29809  wspniunwspnon  29853  trlsegvdeglem1  30149  frcond4  30199  2clwwlk2clwwlk  30279  opabssi  32541  nn0xmulclb  32694  zarclsiin  33861  cusgr3cyclex  35123  satfun  35398  fundmpss  35754  nn0prpw  36311  bj-restpw  37080  bj-prmoore  37103  domalom  37392  cover2  37709  disjlem18  38792  sticksstones11  42144  setindtr  43013  onov0suclim  43263  oe0suclim  43266  ofoaid1  43347  ofoaid2  43348  naddcnfcom  43355  naddcnfass  43358  omssaxinf2  44978  climxlim2lem  45843  sge0f1o  46380  2reuimp  47116  fvelsetpreimafv  47388  imasetpreimafvbijlemfo  47406  reupr  47523  lighneallem4  47611  proththd  47615  lincresunit3  48470  oppc1stflem  49276