Theorem 3impia 1133

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 458	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1132	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mopick2  2671  ceqsalt  3496  3gencl  3506  vtoclgft  3529  rspc6v  3611  mob2  3687  moi  3690  reupick3  4291  disjne  4421  elpr2elpr  4838  disji2  5097  disji  5098  tz7.2  5645  sofld  6186  ordintdif  6413  funopg  6571  fvun1  6973  fvopab6  7025  fveqressseq  7075  fvcofneq  7089  fprg  7153  isores3  7334  ovmpt4g  7558  ovmpos  7559  ov2gf  7560  ofrval  7687  sorpssuni  7730  sorpssint  7731  poxp  8123  poseq  8153  suppss2  8195  frrlem12  8293  smoel  8346  smoord  8351  smogt  8353  oaass  8545  oewordi  8576  oeoalem  8581  oeoelem  8583  nnawordi  8606  nnaass  8607  naddssim  8671  qsel  8793  xpdom3  9062  onsdominel  9113  mapdom3  9136  sdomdomtrfi  9184  domsdomtrfi  9185  php  9190  onomeneq  9197  fisseneq  9222  fodomfir  9286  cantnflem1  9657  ttrclss  9688  cfslbn  10250  cfsmolem  10253  cfcoflem  10255  infpssrlem4  10289  fin23lem7  10299  fin23lem25  10307  isf34lem7  10362  hsmexlem2  10410  axcc3  10421  axdc4lem  10438  tskss  10742  gruss  10780  gruurn  10782  gruiun  10783  gruel  10787  gruen  10796  grudomon  10801  grothac  10814  axpre-sup  11153  axsup  11284  addn0nid  11633  letrp1  12058  p1le  12059  lemul1a  12068  infrelb  12199  nnadddir  12291  zextle  12668  zextlt  12669  btwnnz  12671  gtndiv  12672  uzind2  12688  fzind  12693  zsupss  12960  xrltne  13187  lemaxle  13220  qbtwnre  13224  qbtwnxr  13225  xlemul1a  13313  icogelb  13422  iccleub  13427  iccsplit  13511  uzsubsubfz  13573  elfz0fzfz0  13660  difelfznle  13669  fvffz0  13673  elfzo0le  13731  fzonmapblen  13736  fzofzim  13737  ceile  13881  modadd1  13940  muladdmodid  13945  modmul1  13959  modirr  13977  fsuppmapnn0fiub0  14028  expcl2lem  14108  expclzlem  14118  expnegz  14131  leexp2r  14209  bcval4  14342  bccmpl  14344  hashbnd  14371  hashunsnggt  14429  hashgt23el  14460  hashfundm  14478  elovmpowrd  14594  ccatval2  14614  ccatrcl1  14631  wrdl1s1  14651  ccat2s1fvw  14675  swrdsb0eq  14700  swrdccatin1  14761  pfxccatpfx2  14773  repswswrd  14820  cshwcsh2id  14864  sgn3da  15137  absexpz  15355  climbdd  15722  iseraltlem2  15733  binomfallfac  16094  dvdsle  16367  divalgb  16461  ndvdssub  16466  dvdsgcd  16601  dfgcd2  16603  rplpwr  16615  nn0rppwr  16618  nn0expgcd  16621  lcmgcdlem  16663  lcmfunsn  16701  coprmdvds1  16709  qredeq  16714  2mulprm  16750  prmdvdsexpr  16775  nnnn0modprm0  16865  prm23ge5  16874  pcexp  16918  difsqpwdvds  16946  prmpwdvds  16963  ramcl  17088  cshwshashlem3  17156  cshwrepswhash1  17161  elrestr  17480  mreintcl  17646  mremre  17655  mrieqv2d  17694  initoeu2lem1  18070  funcestrcsetclem9  18203  funcsetcestrclem9  18218  prstr  18354  drsdirfi  18360  latnlej  18511  latnlej2  18514  acsdrsel  18598  acsdrscl  18601  mrelatglb  18615  mrelatlub  18617  isnmgm  18701  grpasscan1  19067  grpinvnz  19075  mulgneg2  19173  gsmsymgrfix  19497  f1omvdco2  19517  symggen  19539  odcl2  19634  odhash3  19645  lsmss1  19734  lsmss2  19736  efgred  19817  efgcpbl  19825  ablfacrp  20137  ablfac1eu  20144  ablfaclem3  20158  omndadd  20197  ogrpaddlt  20207  dvdsrmul1  20450  dvdsunit  20460  irredmul  20510  c0snmgmhm  20543  lmodlema  20963  psgnodpmr  21708  phlssphl  21777  lindsss  21942  lindfmm  21945  ply1scln0  22420  dmatelnd  22621  mdetdiaglem  22723  mdet0  22731  mdetunilem7  22743  slesolinv  22805  cramerimplem3  22810  cpmatpmat  22835  m2cpminvid2lem  22879  chfacfscmul0  22983  chfacfpmmul0  22987  riinopn  23033  clsndisj  23200  cnpf2  23375  hausnei2  23478  cmpcov  23514  cmpfii  23534  unconn  23554  t1connperf  23561  nrmr0reg  23874  fbfinnfr  23966  filuni  24010  alexsubALT  24176  tmdgsum  24220  cuspcvg  24425  mopni  24617  isngp4  24737  metdsre  24979  iimulcl  25064  phtpc01  25123  clmmulg  25228  cfilucfil4  25448  bcthlem5  25455  bcth  25456  bcth3  25458  itg1le  25840  itg2le  25866  bddmulibl  25966  bddiblnc  25969  dvnres  26058  cpnord  26062  dvnfre  26079  deg1ge  26223  dgr1term  26385  aaliou3lem2  26472  sincosq1lem  26627  cxpge0  26813  cxpmul2  26819  logrec  26893  logbgcd1irr  26924  sqfpc  27266  bcmono  27406  gausslemma2dlem1a  27494  gausslemma2dlem2  27496  gausslemma2dlem4  27498  2lgsoddprmlem3  27543  pntrmax  27693  qabvexp  27755  ostth2lem2  27763  nosepon  27794  nolesgn2o  27800  nogesgn1o  27802  nosepnelem  27808  nosepne  27809  nosepdmlem  27812  nosepdm  27813  nodenselem8  27820  noresle  27826  noetasuplem4  27865  noetainflem4  27869  cutbdaylt  27956  eqcuts3  27962  addsuniflem  28159  sltmuls1  28305  precsexlem6  28370  precsexlem7  28371  precsexlem11  28375  ltonold  28419  onnolt  28424  n0fincut  28513  oldfib  28535  expadds  28593  ax5seglem4  29222  axeuclidlem  29252  uhgredgrnv  29420  usgredg4  29507  nbuhgr2vtx1edgblem  29641  vtxduhgr0e  29768  vtxduhgr0nedg  29782  rusgrpropnb  29873  uspgr2wlkeqi  29937  redwlklem  29959  lfgrwlkprop  29975  2pthnloop  30020  spthonepeq  30041  pthdlem2lem  30056  crctcshwlkn0lem3  30101  crctcshwlkn0lem5  30103  crctcshwlkn0lem7  30105  crctcshwlkn0  30110  wlkiswwlks1  30156  wlkiswwlks2  30164  wlkiswwlksupgr2  30166  wwlksnext  30182  wwlksnextproplem2  30199  wspthsnonn0vne  30206  2pthon3v  30232  rusgrnumwwlk  30267  erclwwlkeqlen  30310  erclwwlksym  30312  erclwwlktr  30313  erclwwlkneqlen  30359  erclwwlknsym  30361  erclwwlkntr  30362  uhgr3cyclex  30473  upgreupthseg  30500  eupth2lem3lem4  30522  eucrctshift  30534  4cycl2vnunb  30581  nvs  30955  nvtri  30962  nmlno0  31087  nmlnoubi  31088  ubth  31165  hlipgt0  31206  ocnel  31590  elspansn2  31859  elspansn3  31864  normcan  31868  pjoml2  31903  lecm  31909  osum  31937  nmbdfnlb  32342  leopmul  32426  hstpyth  32521  cvnbtwn  32578  ssmd1  32603  ssmd2  32604  ssdmd1  32605  ssdmd2  32606  cvmd  32628  cvdmd  32629  superpos  32646  disji2f  32862  disjif  32863  disjif2  32866  preiman0  32995  padct  33003  ffs2  33012  bcm1n  33080  s2f1  33205  archiabl  33458  slmdlema  33463  lbslsat  33950  eulerpartlemb  34702  fisshasheq  35504  cvmsdisj  35660  cvmlift2lem12  35704  satfrel  35757  satfrnmapom  35760  fmlasuc  35776  satffun  35799  satef  35806  sategoelfv  35810  lineintmo  36547  nn0prpwlem  36721  nn0prpw  36722  neibastop2lem  36759  tr0elw  36883  lindsadd  38151  areacirc  38251  incsequz  38286  mettrifi  38295  ismtybnd  38345  heiborlem1  38349  rngoisocnv  38519  risci  38525  eqvrelqsel  39238  lfl1  39733  lkrlsp2  39766  omlfh3N  39922  cvrnbtwn  39934  cvrnbtwn2  39938  cvrnbtwn4  39942  cvlexch3  39995  cvlexch4N  39996  cvlatexchb1  39997  2llnne2N  40071  atcvrj0  40091  cvrat2  40092  ps-1  40140  3atlem5  40150  islln2a  40180  lplnriaN  40213  lplnribN  40214  llncvrlpln2  40220  lplncvrlvol2  40278  psubatN  40418  pmapglb2N  40434  pmapglb2xN  40435  2llnma1b  40449  paddasslem17  40499  pmod2iN  40512  pmodl42N  40514  hlmod1i  40519  atmod1i1  40520  atmod1i2  40522  llnmod1i2  40523  pclcmpatN  40564  osumcllem8N  40626  pexmidlem3N  40635  pl42lem4N  40645  4atexlem7  40738  ltrnnid  40799  cdlemc4  40857  cdleme32a  41104  cdlemeg46gfre  41195  cdlemf2  41225  cdlemg4c  41275  trlcoat  41386  tendovalco  41428  tendoeq2  41437  cdlemk36  41576  diael  41706  diatrl  41707  dicelval1stN  41851  dicelval2nd  41852  dihlspsnat  41996  dochkr1  42141  lcfrlem9  42213  mapdh8e  42447  hdmapval0  42496  hgmapval0  42555  dvdsexpnn0  42984  incssnn0  43333  pell14qrexpcl  43485  pell14qrgap  43493  congadd  43584  acongsym  43594  acongtr  43596  dvdsacongtr  43602  jm2.19lem3  43609  jm2.19lem4  43610  jm2.26lem3  43619  onexlimgt  43861  nadd2rabex  44004  ismnushort  44902  bi13impia  45089  3impcombi  45416  ioogtlb  46102  iocgtlb  46109  iocleub  46110  icoltub  46115  iooltub  46117  limclner  46256  limsupre3lem  46337  climuzlem  46348  fsupdm  47447  finfdm  47451  elfzelfzlble  47946  subsubelfzo0  47952  m1modnep2mod  47983  m1modmmod  47989  modlt0b  47994  mod2addne  47995  iccpartigtl  48060  sqrtpwpw2p  48178  fmtnoprmfac1lem  48204  fmtno4prmfac  48212  evenltle  48370  even3prm2  48372  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  bgoldbtbndlem1  48458  bgoldbtbndlem3  48460  bgoldbtbndlem4  48461  bgoldbtbnd  48462  uhgrimisgrgriclem  48583  isubgr3stgrlem7  48625  clnbgr3stgrgrlic  48673  gpgedg2iv  48720  pgnbgreunbgrlem3  48771  pgnbgreunbgrlem6  48777  upgrwlkupwlk  48793  funcringcsetcALTV2lem9  48951  funcringcsetclem9ALTV  48974  lincscmcl  49096  lindslinindimp2lem4  49125  lincresunit2  49142  lincresunit3  49145  elfzolborelfzop1  49183  rege1logbzge0  49223  fllog2  49232  dignn0ldlem  49266  rrx2pnecoorneor  49379  rrx2plord2  49386  rrx2linest  49406  ipolub  49650  ipoglb  49653